---

Step * of Lemma setmem-iff

∀x,s:coSet{i:l}.  ((x ∈ s) ⇐⇒ ∃t:set-dom(s). seteq(x;set-item(s;t)))
BY
{ (Intros
   THEN coSetD 2
   THEN D 2
   THEN RepUR ``setmem coWmem coW-dom coW-item`` 0
   THEN RepUR ``set-dom set-item`` 0
   THEN Fold `seteq` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,s:coSet\{i:l\}.    ((x  \mmember{}  s)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:set-dom(s).  seteq(x;set-item(s;t)))


By

---

Latex:
(Intros
  THEN  coSetD  2
  THEN  D  2
  THEN  RepUR  ``setmem  coWmem  coW-dom  coW-item``  0
  THEN  RepUR  ``set-dom  set-item``  0
  THEN  Fold  `seteq`  0
  THEN  Auto)

---

Home Index