---

Step * of Lemma assert_of_dset_eq

∀[s:DSet]. ∀[a,b:|s|].  uiff(↑(a (=b) b);a = b ∈ |s|)
BY
{ ((UnivCD) THENA Auto) }

1
1. s : DSet
2. a : |s|
3. b : |s|
⊢ uiff(↑(a (=b) b);a = b ∈ |s|)

---

Latex:

---

Latex:
\mforall{}[s:DSet].  \mforall{}[a,b:|s|].    uiff(\muparrow{}(a  (=\msubb{})  b);a  =  b)


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index