Metamath Proof Explorer
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 
$${\u22a2}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to {B}\in \mathrm{V}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

brrelex12 
$${\u22a2}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$$ 
2 
1

simprd 
$${\u22a2}\left(\mathrm{Rel}{R}\wedge {A}{R}{B}\right)\to {B}\in \mathrm{V}$$ 