This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brrelex12i

Description: Two classes that are related by a binary relation are sets. Inference form. (Contributed by BJ, 3-Oct-2022)

Ref Expression
Hypothesis brrelexi.1 ⊢ Rel ⁡ R
Assertion brrelex12i ⊢ A R B → A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 brrelexi.1 ⊢ Rel ⁡ R
2 brrelex12 ⊢ Rel ⁡ R ∧ A R B → A ∈ V ∧ B ∈ V
3 1 2 mpan ⊢ A R B → A ∈ V ∧ B ∈ V