∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} {x : (i : ι) → φ i},
  (x ∈ Submodule.pi I p) = ∀ i ∈ I, x i ∈ p i