Theorem cbvopab1s

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 31-Jul-2003)

	Ref	Expression
Assertion	cbvopab1s	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,y⟩|\left[z/x\right]\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎz\exists y\left(w=⟨x,y⟩\wedge \phi \right)$$
2		nfv	$$⊢Ⅎxw=⟨z,y⟩$$
3		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
4	2 3	nfan	$$⊢Ⅎx\left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)$$
5	4	nfex	$$⊢Ⅎx\exists y\left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)$$
6		opeq1	$$⊢x=z\to ⟨x,y⟩=⟨z,y⟩$$
7	6	eqeq2d	$$⊢x=z\to \left(w=⟨x,y⟩\leftrightarrow w=⟨z,y⟩\right)$$
8		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
9	7 8	anbi12d	$$⊢x=z\to \left(\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)\right)$$
10	9	exbidv	$$⊢x=z\to \left(\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)\right)$$
11	1 5 10	cbvexv1	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\exists y\left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)$$
12	11	abbii	$$⊢\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{w|\exists z\exists y\left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)\right\}$$
13		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
14		df-opab	$$⊢\left\{⟨z,y⟩|\left[z/x\right]\phi \right\}=\left\{w|\exists z\exists y\left(w=⟨z,y⟩\wedge \left[z/x\right]\phi \right)\right\}$$
15	12 13 14	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,y⟩|\left[z/x\right]\phi \right\}$$