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 V

Proof

Step Hyp Ref Expression
1 brrelex12 Rel R A R B A V B V
2 1 simprd Rel R A R B B V