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