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

Metamath Proof Explorer

Theorem brrpssg

Description: The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion brrpssg 
|- ( B e. V -> ( A [C.] B <-> A C. B ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( B e. V -> B e. _V )
2 relrpss 
 |-  Rel [C.]
3 2 brrelex1i 
 |-  ( A [C.] B -> A e. _V )
4 1 3 anim12i 
 |-  ( ( B e. V /\ A [C.] B ) -> ( B e. _V /\ A e. _V ) )
5 1 adantr 
 |-  ( ( B e. V /\ A C. B ) -> B e. _V )
6 pssss 
 |-  ( A C. B -> A C_ B )
7 ssexg 
 |-  ( ( A C_ B /\ B e. _V ) -> A e. _V )
8 6 1 7 syl2anr 
 |-  ( ( B e. V /\ A C. B ) -> A e. _V )
9 5 8 jca 
 |-  ( ( B e. V /\ A C. B ) -> ( B e. _V /\ A e. _V ) )
10 psseq1 
 |-  ( x = A -> ( x C. y <-> A C. y ) )
11 psseq2 
 |-  ( y = B -> ( A C. y <-> A C. B ) )
12 df-rpss 
 |-  [C.] = { <. x , y >. | x C. y }
13 10 11 12 brabg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A [C.] B <-> A C. B ) )
14 13 ancoms 
 |-  ( ( B e. _V /\ A e. _V ) -> ( A [C.] B <-> A C. B ) )
15 4 9 14 pm5.21nd 
 |-  ( B e. V -> ( A [C.] B <-> A C. B ) )