---

Step * of Lemma f-singleton-subset

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[a:A]. ∀[x:fset(A)].  uiff({a} ⊆ x;a ∈ x)
BY
{ ((UnivCD THENA Auto) THEN Unfold `f-subset` 0 THEN RWO "member-fset-singleton" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[a:A].  \mforall{}[x:fset(A)].    uiff(\{a\}  \msubseteq{}  x;a  \mmember{}  x)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `f-subset`  0  THEN  RWO  "member-fset-singleton"  0  THEN  Auto)

---

Home Index