Theorem brrelex12

Description: Two classes related by a binary relation are sets. (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	brrelex12	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		df-rel	⊢ ( Rel 𝑅 ↔ 𝑅 ⊆ ( V × V ) )
2	1	biimpi	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( V × V ) )
3	2	ssbrd	⊢ ( Rel 𝑅 → ( 𝐴 𝑅 𝐵 → 𝐴 ( V × V ) 𝐵 ) )
4	3	imp	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ( V × V ) 𝐵 )
5		brxp	⊢ ( 𝐴 ( V × V ) 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
6	4 5	sylib	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )