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

Metamath Proof Explorer

Theorem brabv

Description: If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017)

Ref Expression
Assertion brabv 
|- ( X { <. x , y >. | ph } Y -> ( X e. _V /\ Y e. _V ) )

Proof

Step Hyp Ref Expression
1 df-br 
 |-  ( X { <. x , y >. | ph } Y <-> <. X , Y >. e. { <. x , y >. | ph } )
2 opprc 
 |-  ( -. ( X e. _V /\ Y e. _V ) -> <. X , Y >. = (/) )
3 0nelopab 
 |-  -. (/) e. { <. x , y >. | ph }
4 eleq1 
 |-  ( <. X , Y >. = (/) -> ( <. X , Y >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
5 3 4 mtbiri 
 |-  ( <. X , Y >. = (/) -> -. <. X , Y >. e. { <. x , y >. | ph } )
6 2 5 syl 
 |-  ( -. ( X e. _V /\ Y e. _V ) -> -. <. X , Y >. e. { <. x , y >. | ph } )
7 6 con4i 
 |-  ( <. X , Y >. e. { <. x , y >. | ph } -> ( X e. _V /\ Y e. _V ) )
8 1 7 sylbi 
 |-  ( X { <. x , y >. | ph } Y -> ( X e. _V /\ Y e. _V ) )