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