---

Step * 1 of Lemma setmem-natset


1. x : Set{i:l}
2. (x ∈ natset(0))
⊢ ∃i:ℕ0. seteq(x;natset(i))
BY
{ (Unfold `natset` -1 THEN Reduce -1 THEN SetMemDef (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  Set\{i:l\}
2.  (x  \mmember{}  natset(0))
\mvdash{}  \mexists{}i:\mBbbN{}0.  seteq(x;natset(i))


By

---

Latex:
(Unfold  `natset`  -1  THEN  Reduce  -1  THEN  SetMemDef  (-1)  THEN  Auto)

---

Home Index