---

Step * of Lemma exists-simp

∀[T:Type]. ∀a:T. ∀P:T ⟶ ℙ.  ((∀x:T. (P[x] ⇒ (x = a ∈ T))) ⇒ (∃x:T. P[x] ⇐⇒ P[a]))
BY
{ (Auto THEN ExRepD THEN Try ((FHyp (-3) [-1] THEN Auto)) THEN With ⌜a⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  ExRepD  THEN  Try  ((FHyp  (-3)  [-1]  THEN  Auto))  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index