---

Step * of Lemma exists-elim

∀[T:Type]. ∀[P:T ⟶ ℙ'].  ∀a:T. ((∀x:T. (P[x] ⇒ (x = a ∈ T))) ⇒ {∃x:T. P[x] ⇐⇒ P[a]})
BY
{ (Unfold `guard` 0 THEN Auto THEN ExRepD THEN FHyp (-3) [-1] THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto  THEN  ExRepD  THEN  FHyp  (-3)  [-1]  THEN  Auto)

---

Home Index