---

Step * 1 of Lemma assert_of_dset_eq


1. s : DSet
2. a : |s|
3. b : |s|
⊢ uiff(↑(a (=b) b);a = b ∈ |s|)
BY
{ AddProperties 1 
THEN UnfoldTopAb 2 
 }

1
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|)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  b  :  |s|
\mvdash{}  uiff(\muparrow{}(a  (=\msubb{})  b);a  =  b)


By

---

Latex:
AddProperties  1 
THEN  UnfoldTopAb  2 

---

Home Index