---

Step * of Lemma classical-exists1

∀[T:Type]. ∀[P:T ⟶ ℙ].  ((∃x:T. {P[x]}) ⇒ {∃x:T. P[x]})
BY
{ (Auto THEN ExRepD THEN (ExposeClassical THENA Auto) THEN ElimClassical THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    ((\mexists{}x:T.  \{P[x]\})  {}\mRightarrow{}  \{\mexists{}x:T.  P[x]\})


By

---

Latex:
(Auto  THEN  ExRepD  THEN  (ExposeClassical  THENA  Auto)  THEN  ElimClassical  THEN  Auto)

---

Home Index