Theorem vopelopabsb

Description: The law of concretion in terms of substitutions. Version of opelopabsb with set variables. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) Remove unnecessary commutation. (Revised by SN, 1-Sep-2024)

	Ref	Expression
Assertion	vopelopabsb	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/x\right]\left[w/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢⟨z,w⟩=⟨x,y⟩\leftrightarrow ⟨x,y⟩=⟨z,w⟩$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	opth	$$⊢⟨x,y⟩=⟨z,w⟩\leftrightarrow \left(x=z\wedge y=w\right)$$
5	1 4	bitri	$$⊢⟨z,w⟩=⟨x,y⟩\leftrightarrow \left(x=z\wedge y=w\right)$$
6	5	anbi1i	$$⊢\left(⟨z,w⟩=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(\left(x=z\wedge y=w\right)\wedge \phi \right)$$
7	6	2exbii	$$⊢\exists x\exists y\left(⟨z,w⟩=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(\left(x=z\wedge y=w\right)\wedge \phi \right)$$
8		elopab	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \exists x\exists y\left(⟨z,w⟩=⟨x,y⟩\wedge \phi \right)$$
9		2sb5	$$⊢\left[z/x\right]\left[w/y\right]\phi \leftrightarrow \exists x\exists y\left(\left(x=z\wedge y=w\right)\wedge \phi \right)$$
10	7 8 9	3bitr4i	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/x\right]\left[w/y\right]\phi$$