Metamath Proof Explorer

Theorem brrelex2

Description: If two classes are related by a binary relation, then the second class is a set. (Contributed by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 brrelex12 
 |-  ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) )
2 1 simprd 
 |-  ( ( Rel R /\ A R B ) -> B e. _V )