Metamath Proof Explorer


Theorem brrelex1

Description: If two classes are related by a binary relation, then the first class is a set. (Contributed by NM, 18-May-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion brrelex1 RelRARBAV

Proof

Step Hyp Ref Expression
1 brrelex12 RelRARBAVBV
2 1 simpld RelRARBAV