# Metamath Proof Explorer

## Theorem bropaex12

Description: Two classes related by an ordered-pair class abstraction are sets. (Contributed by AV, 21-Jan-2020)

Ref Expression
Hypothesis bropaex12.1 ${⊢}{R}=\left\{⟨{x},{y}⟩|{\psi }\right\}$
Assertion bropaex12 ${⊢}{A}{R}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$

### Proof

Step Hyp Ref Expression
1 bropaex12.1 ${⊢}{R}=\left\{⟨{x},{y}⟩|{\psi }\right\}$
2 df-br ${⊢}{A}{R}{B}↔⟨{A},{B}⟩\in {R}$
3 1 eleq2i ${⊢}⟨{A},{B}⟩\in {R}↔⟨{A},{B}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}$
4 2 3 bitri ${⊢}{A}{R}{B}↔⟨{A},{B}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}$
5 elopaelxp ${⊢}⟨{A},{B}⟩\in \left\{⟨{x},{y}⟩|{\psi }\right\}\to ⟨{A},{B}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
6 4 5 sylbi ${⊢}{A}{R}{B}\to ⟨{A},{B}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
7 opelxp ${⊢}⟨{A},{B}⟩\in \left(\mathrm{V}×\mathrm{V}\right)↔\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
8 6 7 sylib ${⊢}{A}{R}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$