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

Metamath Proof Explorer

Theorem bropaex12

Description: Two classes related by an ordered-pair class abstraction are sets. (Contributed by AV, 21-Jan-2020)

Ref Expression
Hypothesis bropaex12.1 
|- R = { <. x , y >. | ps }
Assertion bropaex12 
|- ( A R B -> ( A e. _V /\ B e. _V ) )

Proof

Step Hyp Ref Expression
1 bropaex12.1 
 |-  R = { <. x , y >. | ps }
2 df-br 
 |-  ( A R B <-> <. A , B >. e. R )
3 1 eleq2i 
 |-  ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ps } )
4 2 3 bitri 
 |-  ( A R B <-> <. A , B >. e. { <. x , y >. | ps } )
5 elopaelxp 
 |-  ( <. A , B >. e. { <. x , y >. | ps } -> <. A , B >. e. ( _V X. _V ) )
6 4 5 sylbi 
 |-  ( A R B -> <. A , B >. e. ( _V X. _V ) )
7 opelxp 
 |-  ( <. A , B >. e. ( _V X. _V ) <-> ( A e. _V /\ B e. _V ) )
8 6 7 sylib 
 |-  ( A R B -> ( A e. _V /\ B e. _V ) )