Theorem opelopab4

Description: Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 6-May-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	opelopab4	$$⊢⟨u,v⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(\left(x=u\wedge y=v\right)\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elopab	$$⊢⟨u,v⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(⟨u,v⟩=⟨x,y⟩\wedge \phi \right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	opth	$$⊢⟨x,y⟩=⟨u,v⟩\leftrightarrow \left(x=u\wedge y=v\right)$$
5		eqcom	$$⊢⟨x,y⟩=⟨u,v⟩\leftrightarrow ⟨u,v⟩=⟨x,y⟩$$
6	4 5	bitr3i	$$⊢\left(x=u\wedge y=v\right)\leftrightarrow ⟨u,v⟩=⟨x,y⟩$$
7	6	anbi1i	$$⊢\left(\left(x=u\wedge y=v\right)\wedge \phi \right)\leftrightarrow \left(⟨u,v⟩=⟨x,y⟩\wedge \phi \right)$$
8	7	2exbii	$$⊢\exists x\exists y\left(\left(x=u\wedge y=v\right)\wedge \phi \right)\leftrightarrow \exists x\exists y\left(⟨u,v⟩=⟨x,y⟩\wedge \phi \right)$$
9	1 8	bitr4i	$$⊢⟨u,v⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(\left(x=u\wedge y=v\right)\wedge \phi \right)$$