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

Metamath Proof Explorer

Theorem brssr

Description: The subset relation and subclass relationship ( df-ss ) are the same, that is, ( AS B <-> A C B ) when B is a set. (Contributed by Peter Mazsa, 31-Jul-2019)

Ref Expression
Assertion brssr 
|- ( B e. V -> ( A _S B <-> A C_ B ) )

Proof

Step Hyp Ref Expression
1 relssr 
 |-  Rel _S
2 1 brrelex1i 
 |-  ( A _S B -> A e. _V )
3 2 adantl 
 |-  ( ( B e. V /\ A _S B ) -> A e. _V )
4 simpl 
 |-  ( ( B e. V /\ A _S B ) -> B e. V )
5 3 4 jca 
 |-  ( ( B e. V /\ A _S B ) -> ( A e. _V /\ B e. V ) )
6 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
7 simpr 
 |-  ( ( A C_ B /\ B e. V ) -> B e. V )
8 6 7 jca 
 |-  ( ( A C_ B /\ B e. V ) -> ( A e. _V /\ B e. V ) )
9 8 ancoms 
 |-  ( ( B e. V /\ A C_ B ) -> ( A e. _V /\ B e. V ) )
10 sseq1 
 |-  ( x = A -> ( x C_ y <-> A C_ y ) )
11 sseq2 
 |-  ( y = B -> ( A C_ y <-> A C_ B ) )
12 df-ssr 
 |-  _S = { <. x , y >. | x C_ y }
13 10 11 12 brabg 
 |-  ( ( A e. _V /\ B e. V ) -> ( A _S B <-> A C_ B ) )
14 5 9 13 pm5.21nd 
 |-  ( B e. V -> ( A _S B <-> A C_ B ) )