Theorem cbvopab1

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See cbvopab1g for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024)

	Ref	Expression
Hypotheses	cbvopab1.1	$$⊢Ⅎz\phi$$
	cbvopab1.2	$$⊢Ⅎx\psi$$
	cbvopab1.3	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvopab1	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,y⟩|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvopab1.1	$$⊢Ⅎz\phi$$
2		cbvopab1.2	$$⊢Ⅎx\psi$$
3		cbvopab1.3	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
4		nfv	$$⊢Ⅎv\exists y\left(w=⟨x,y⟩\wedge \phi \right)$$
5		nfv	$$⊢Ⅎxw=⟨v,y⟩$$
6		nfs1v	$$⊢Ⅎx\left[v/x\right]\phi$$
7	5 6	nfan	$$⊢Ⅎx\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)$$
8	7	nfex	$$⊢Ⅎx\exists y\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)$$
9		opeq1	$$⊢x=v\to ⟨x,y⟩=⟨v,y⟩$$
10	9	eqeq2d	$$⊢x=v\to \left(w=⟨x,y⟩\leftrightarrow w=⟨v,y⟩\right)$$
11		sbequ12	$$⊢x=v\to \left(\phi \leftrightarrow \left[v/x\right]\phi \right)$$
12	10 11	anbi12d	$$⊢x=v\to \left(\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)\right)$$
13	12	exbidv	$$⊢x=v\to \left(\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)\right)$$
14	4 8 13	cbvexv1	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists v\exists y\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)$$
15		nfv	$$⊢Ⅎzw=⟨v,y⟩$$
16	1	nfsbv	$$⊢Ⅎz\left[v/x\right]\phi$$
17	15 16	nfan	$$⊢Ⅎz\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)$$
18	17	nfex	$$⊢Ⅎz\exists y\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)$$
19		nfv	$$⊢Ⅎv\exists y\left(w=⟨z,y⟩\wedge \psi \right)$$
20		opeq1	$$⊢v=z\to ⟨v,y⟩=⟨z,y⟩$$
21	20	eqeq2d	$$⊢v=z\to \left(w=⟨v,y⟩\leftrightarrow w=⟨z,y⟩\right)$$
22	2 3	sbhypf	$$⊢v=z\to \left(\left[v/x\right]\phi \leftrightarrow \psi \right)$$
23	21 22	anbi12d	$$⊢v=z\to \left(\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)\leftrightarrow \left(w=⟨z,y⟩\wedge \psi \right)\right)$$
24	23	exbidv	$$⊢v=z\to \left(\exists y\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)\leftrightarrow \exists y\left(w=⟨z,y⟩\wedge \psi \right)\right)$$
25	18 19 24	cbvexv1	$$⊢\exists v\exists y\left(w=⟨v,y⟩\wedge \left[v/x\right]\phi \right)\leftrightarrow \exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)$$
26	14 25	bitri	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)$$
27	26	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 \psi \right)\right\}$$
28		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
29		df-opab	$$⊢\left\{⟨z,y⟩|\psi \right\}=\left\{w|\exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)\right\}$$
30	27 28 29	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,y⟩|\psi \right\}$$