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

Assertion  brrelex2   ( ( Rel R /\ A R B ) > B e. _V ) 
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 ) 