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 ( ( Rel 𝑅𝐴 𝑅 𝐵 ) → 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 brrelex12 ( ( Rel 𝑅𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
2 1 simpld ( ( Rel 𝑅𝐴 𝑅 𝐵 ) → 𝐴 ∈ V )