Step * 1 1 of Lemma assert_of_dset_eq


1. DSet
2. ∀[x,y:|s|].  uiff(↑(x (=by);x y ∈ |s|)
3. |s|
4. |s|
⊢ uiff(↑(a (=bb);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