Theorem cbvopab2

Description: Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab2.1	$$⊢Ⅎz\phi$$
2		cbvopab2.2	$$⊢Ⅎy\psi$$
3		cbvopab2.3	$$⊢y=z\to \left(\phi \leftrightarrow \psi \right)$$
4		nfv	$$⊢Ⅎzw=⟨x,y⟩$$
5	4 1	nfan	$$⊢Ⅎz\left(w=⟨x,y⟩\wedge \phi \right)$$
6		nfv	$$⊢Ⅎyw=⟨x,z⟩$$
7	6 2	nfan	$$⊢Ⅎy\left(w=⟨x,z⟩\wedge \psi \right)$$
8		opeq2	$$⊢y=z\to ⟨x,y⟩=⟨x,z⟩$$
9	8	eqeq2d	$$⊢y=z\to \left(w=⟨x,y⟩\leftrightarrow w=⟨x,z⟩\right)$$
10	9 3	anbi12d	$$⊢y=z\to \left(\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨x,z⟩\wedge \psi \right)\right)$$
11	5 7 10	cbvexv1	$$⊢\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\left(w=⟨x,z⟩\wedge \psi \right)$$
12	11	exbii	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists z\left(w=⟨x,z⟩\wedge \psi \right)$$
13	12	abbii	$$⊢\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}=\left\{w|\exists x\exists z\left(w=⟨x,z⟩\wedge \psi \right)\right\}$$
14		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
15		df-opab	$$⊢\left\{⟨x,z⟩|\psi \right\}=\left\{w|\exists x\exists z\left(w=⟨x,z⟩\wedge \psi \right)\right\}$$
16	13 14 15	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,z⟩|\psi \right\}$$