---

Step * of Lemma f-subset-singleton

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

1
1. [A] : Type
2. [eq] : EqDecider(A)
3. [a] : A
4. x : fset(A)
5. ∀a@0:A. a@0 = a ∈ A supposing a@0 ∈ x
⊢ (x = {a} ∈ fset(A)) ∨ (x = {} ∈ fset(A))

2
1. A : Type
2. eq : EqDecider(A)
3. a : A
4. x : fset(A)
5. (x = {a} ∈ fset(A)) ∨ (x = {} ∈ fset(A))
6. a@0 : A
7. a@0 ∈ x
⊢ a@0 = a ∈ A

---

Latex:

---

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


By

---

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

---

Home Index