---

Step * of Lemma natset-seteq-natset

∀n,m:ℕ.  (seteq(natset(n);natset(m)) ⇐⇒ n = m ∈ ℤ)
BY
{ Auto }

1
1. n : ℕ
2. m : ℕ
3. seteq(natset(n);natset(m))
⊢ n = m ∈ ℤ

2
1. n : ℕ
2. m : ℕ
3. n = m ∈ ℤ
⊢ seteq(natset(n);natset(m))

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbN{}.    (seteq(natset(n);natset(m))  \mLeftarrow{}{}\mRightarrow{}  n  =  m)


By

---

Latex:
Auto

---

Home Index