Theorem brrelex12

Description: Two classes related by a binary relation are sets. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	brrelex12	|- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		df-rel	|- ( Rel R <-> R C_ ( _V X. _V ) )
2	1	biimpi	|- ( Rel R -> R C_ ( _V X. _V ) )
3	2	ssbrd	|- ( Rel R -> ( A R B -> A ( _V X. _V ) B ) )
4	3	imp	|- ( ( Rel R /\ A R B ) -> A ( _V X. _V ) B )
5		brxp	|- ( A ( _V X. _V ) B <-> ( A e. _V /\ B e. _V ) )
6	4 5	sylib	|- ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )