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 ) )