---

Step * of Lemma setmem-mkset

∀T:Type. ∀f:T ⟶ Set{i:l}. ∀x:Set{i:l}.  ((x ∈ {f[t] | t ∈ T}) ⇐⇒ ∃t:T. seteq(x;f[t]))
BY
{ (Intros THEN (RWO "setmem-iff" 0 THENA Auto) THEN RepUR ``mkset set-dom set-item`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  Set\{i:l\}.  \mforall{}x:Set\{i:l\}.    ((x  \mmember{}  \{f[t]  |  t  \mmember{}  T\})  \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:T.  seteq(x;f[t]))


By

---

Latex:
(Intros  THEN  (RWO  "setmem-iff"  0  THENA  Auto)  THEN  RepUR  ``mkset  set-dom  set-item``  0  THEN  Auto)

---

Home Index