This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brsset

Description: For sets, the SSet binary relation is equivalent to the subset relationship. (Contributed by Scott Fenton, 31-Mar-2012)

Ref Expression
Hypothesis brsset.1 
|- B e. _V
Assertion brsset 
|- ( A SSet B <-> A C_ B )

Proof

Step Hyp Ref Expression
1 brsset.1 
 |-  B e. _V
2 relsset 
 |-  Rel SSet
3 2 brrelex1i 
 |-  ( A SSet B -> A e. _V )
4 1 ssex 
 |-  ( A C_ B -> A e. _V )
5 breq1 
 |-  ( x = A -> ( x SSet B <-> A SSet B ) )
6 sseq1 
 |-  ( x = A -> ( x C_ B <-> A C_ B ) )
7 opex 
 |-  <. x , B >. e. _V
8 7 elrn 
 |-  ( <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) <-> E. y y ( _E (x) ( _V \ _E ) ) <. x , B >. )
9 vex 
 |-  y e. _V
10 vex 
 |-  x e. _V
11 9 10 1 brtxp 
 |-  ( y ( _E (x) ( _V \ _E ) ) <. x , B >. <-> ( y _E x /\ y ( _V \ _E ) B ) )
12 epel 
 |-  ( y _E x <-> y e. x )
13 brv 
 |-  y _V B
14 brdif 
 |-  ( y ( _V \ _E ) B <-> ( y _V B /\ -. y _E B ) )
15 13 14 mpbiran 
 |-  ( y ( _V \ _E ) B <-> -. y _E B )
16 1 epeli 
 |-  ( y _E B <-> y e. B )
17 15 16 xchbinx 
 |-  ( y ( _V \ _E ) B <-> -. y e. B )
18 12 17 anbi12i 
 |-  ( ( y _E x /\ y ( _V \ _E ) B ) <-> ( y e. x /\ -. y e. B ) )
19 11 18 bitri 
 |-  ( y ( _E (x) ( _V \ _E ) ) <. x , B >. <-> ( y e. x /\ -. y e. B ) )
20 19 exbii 
 |-  ( E. y y ( _E (x) ( _V \ _E ) ) <. x , B >. <-> E. y ( y e. x /\ -. y e. B ) )
21 exanali 
 |-  ( E. y ( y e. x /\ -. y e. B ) <-> -. A. y ( y e. x -> y e. B ) )
22 8 20 21 3bitrri 
 |-  ( -. A. y ( y e. x -> y e. B ) <-> <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) )
23 22 con1bii 
 |-  ( -. <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) <-> A. y ( y e. x -> y e. B ) )
24 df-br 
 |-  ( x SSet B <-> <. x , B >. e. SSet )
25 df-sset 
 |-  SSet = ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) )
26 25 eleq2i 
 |-  ( <. x , B >. e. SSet <-> <. x , B >. e. ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) ) )
27 10 1 opelvv 
 |-  <. x , B >. e. ( _V X. _V )
28 eldif 
 |-  ( <. x , B >. e. ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) ) <-> ( <. x , B >. e. ( _V X. _V ) /\ -. <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) ) )
29 27 28 mpbiran 
 |-  ( <. x , B >. e. ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) ) <-> -. <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) )
30 26 29 bitri 
 |-  ( <. x , B >. e. SSet <-> -. <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) )
31 24 30 bitri 
 |-  ( x SSet B <-> -. <. x , B >. e. ran ( _E (x) ( _V \ _E ) ) )
32 df-ss 
 |-  ( x C_ B <-> A. y ( y e. x -> y e. B ) )
33 23 31 32 3bitr4i 
 |-  ( x SSet B <-> x C_ B )
34 5 6 33 vtoclbg 
 |-  ( A e. _V -> ( A SSet B <-> A C_ B ) )
35 3 4 34 pm5.21nii 
 |-  ( A SSet B <-> A C_ B )