Theorem cbvopabv

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

	Ref	Expression
Hypothesis	cbvopabv.1	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvopabv	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,w⟩|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvopabv.1	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		opeq12	$$⊢\left(x=z\wedge y=w\right)\to ⟨x,y⟩=⟨z,w⟩$$
3	2	eqeq2d	$$⊢\left(x=z\wedge y=w\right)\to \left(v=⟨x,y⟩\leftrightarrow v=⟨z,w⟩\right)$$
4	3 1	anbi12d	$$⊢\left(x=z\wedge y=w\right)\to \left(\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(v=⟨z,w⟩\wedge \psi \right)\right)$$
5	4	cbvex2vw	$$⊢\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\exists w\left(v=⟨z,w⟩\wedge \psi \right)$$
6	5	abbii	$$⊢\left\{v|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}=\left\{v|\exists z\exists w\left(v=⟨z,w⟩\wedge \psi \right)\right\}$$
7		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{v|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}$$
8		df-opab	$$⊢\left\{⟨z,w⟩|\psi \right\}=\left\{v|\exists z\exists w\left(v=⟨z,w⟩\wedge \psi \right)\right\}$$
9	6 7 8	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,w⟩|\psi \right\}$$