---

Step * of Lemma setmem-funset

∀A,B,x:coSet{i:l}.  ((x ∈ A ⟶ B) ⇐⇒ function-graph{i:l}(A;_.B;x))
BY
{ ((UnivCD THENA Auto) THEN Unfold `funset` 0 THEN RWO "setmem-Piset" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}A,B,x:coSet\{i:l\}.    ((x  \mmember{}  A  {}\mrightarrow{}  B)  \mLeftarrow{}{}\mRightarrow{}  function-graph\{i:l\}(A;$_{}$.B;x))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `funset`  0  THEN  RWO  "setmem-Piset"  0  THEN  Auto)

---

Home Index