---

Step * 1 1 of Lemma assert_of_dset_eq


1. s : DSet
2. ∀[x,y:|s|].  uiff(↑(x (=b) y);x = y ∈ |s|)
3. a : |s|
4. b : |s|
⊢ uiff(↑(a (=b) b);a = b ∈ |s|)
BY
{ Sel (-1) (BHyp 2) THEN Auto }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  \mforall{}[x,y:|s|].    uiff(\muparrow{}(x  (=\msubb{})  y);x  =  y)
3.  a  :  |s|
4.  b  :  |s|
\mvdash{}  uiff(\muparrow{}(a  (=\msubb{})  b);a  =  b)


By

---

Latex:
Sel  (-1)  (BHyp  2)  THEN  Auto

---

Home Index