Metamath Proof Explorer

Theorem brrelex12

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

Ref Expression
Assertion brrelex12 ⊢ Rel ⁡ R ∧ A R B → A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 df-rel ⊢ Rel ⁡ R ↔ R ⊆ V × V
2 1 biimpi ⊢ Rel ⁡ R → R ⊆ V × V
3 2 ssbrd ⊢ Rel ⁡ R → A R B → A V × V B
4 3 imp ⊢ Rel ⁡ R ∧ A R B → A V × V B
5 brxp ⊢ A V × V B ↔ A ∈ V ∧ B ∈ V
6 4 5 sylib ⊢ Rel ⁡ R ∧ A R B → A ∈ V ∧ B ∈ V