---

Step * of Lemma singleitem-singleset

∀a:coSet{i:l}. seteq(singleitem({a});a)
BY
{ (Auto THEN (RWO "co-seteq-iff" 0 THENA Auto) THEN (D 0 THENA Auto)) }

1
1. a : coSet{i:l}
2. z : coSet{i:l}
⊢ (z ∈ singleitem({a})) ⇐⇒ (z ∈ a)

---

Latex:

---

Latex:
\mforall{}a:coSet\{i:l\}.  seteq(singleitem(\{a\});a)


By

---

Latex:
(Auto  THEN  (RWO  "co-seteq-iff"  0  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index