---

Step * of Lemma equipollent-one-iff

∀[A:Type]. (A ~ ℕ1 ⇐⇒ ∃z:A. ∀x:A. (x = z ∈ A))
BY
{ xxxAutoxxx }

1
1. [A] : Type
2. A ~ ℕ1
⊢ ∃z:A. ∀x:A. (x = z ∈ A)

2
1. [A] : Type
2. ∃z:A. ∀x:A. (x = z ∈ A)
⊢ A ~ ℕ1

---

Latex:

---

Latex:
\mforall{}[A:Type].  (A  \msim{}  \mBbbN{}1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}z:A.  \mforall{}x:A.  (x  =  z))


By

---

Latex:
xxxAutoxxx

---

Home Index