Theorem cbvopab1g

Description: Change first bound variable in an ordered-pair class abstraction, using explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbvopab1 for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 6-Oct-2004) (Revised by Mario Carneiro, 14-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab1g.1	$$⊢Ⅎz\phi$$
2		cbvopab1g.2	$$⊢Ⅎx\psi$$
3		cbvopab1g.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	nfsb	$$⊢Ⅎ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		sbequ	$$⊢v=z\to \left(\left[v/x\right]\phi \leftrightarrow \left[z/x\right]\phi \right)$$
23	2 3	sbie	$$⊢\left[z/x\right]\phi \leftrightarrow \psi$$
24	22 23	bitrdi	$$⊢v=z\to \left(\left[v/x\right]\phi \leftrightarrow \psi \right)$$
25	21 24	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)$$
26	25	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)$$
27	18 19 26	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)$$
28	14 27	bitri	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)$$
29	28	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\}$$
30		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
31		df-opab	$$⊢\left\{⟨z,y⟩|\psi \right\}=\left\{w|\exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)\right\}$$
32	29 30 31	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,y⟩|\psi \right\}$$