# Metamath Proof Explorer

## Theorem brabv

Description: If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017)

Ref Expression
Assertion brabv ${⊢}{X}\left\{⟨{x},{y}⟩|{\phi }\right\}{Y}\to \left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 df-br ${⊢}{X}\left\{⟨{x},{y}⟩|{\phi }\right\}{Y}↔⟨{X},{Y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}$
2 opprc ${⊢}¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\to ⟨{X},{Y}⟩=\varnothing$
3 0nelopab ${⊢}¬\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}$
4 eleq1 ${⊢}⟨{X},{Y}⟩=\varnothing \to \left(⟨{X},{Y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}↔\varnothing \in \left\{⟨{x},{y}⟩|{\phi }\right\}\right)$
5 3 4 mtbiri ${⊢}⟨{X},{Y}⟩=\varnothing \to ¬⟨{X},{Y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}$
6 2 5 syl ${⊢}¬\left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\to ¬⟨{X},{Y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}$
7 6 con4i ${⊢}⟨{X},{Y}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}\to \left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$
8 1 7 sylbi ${⊢}{X}\left\{⟨{x},{y}⟩|{\phi }\right\}{Y}\to \left({X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$