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	$$⊢ARB\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	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
3	1	eleq2i	$$⊢⟨A,B⟩\in R\leftrightarrow ⟨A,B⟩\in \left\{⟨x,y⟩|\psi \right\}$$
4	2 3	bitri	$$⊢ARB\leftrightarrow ⟨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}\times \mathrm{V}\right)$$
6	4 5	sylbi	$$⊢ARB\to ⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7		opelxp	$$⊢⟨A,B⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
8	6 7	sylib	$$⊢ARB\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$