---

Step * of Lemma exists_over_and_r

∀[T:Type]. ∀[A:ℙ]. ∀[B:T ⟶ ℙ].  (∃x:T. (A ∧ B[x]) ⇐⇒ A ∧ (∃x:T. B[x]))
BY
{ (GenExRepD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A:\mBbbP{}].  \mforall{}[B:T  {}\mrightarrow{}  \mBbbP{}].    (\mexists{}x:T.  (A  \mwedge{}  B[x])  \mLeftarrow{}{}\mRightarrow{}  A  \mwedge{}  (\mexists{}x:T.  B[x]))


By

---

Latex:
(GenExRepD  THEN  Auto)

---

Home Index