---

Step * of Lemma bag-member-single

∀[T:Type]. ∀[x,y:T].  uiff(x ↓∈ {y};x = y ∈ T)
BY
{ Auto }

1
1. T : Type
2. x : T
3. y : T
4. x ↓∈ {y}
⊢ x = y ∈ T

2
1. T : Type
2. x : T
3. y : T
4. x = y ∈ T
⊢ x ↓∈ {y}

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x,y:T].    uiff(x  \mdownarrow{}\mmember{}  \{y\};x  =  y)


By

---

Latex:
Auto

---

Home Index