Theorem cbvopab1v

Description: Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003) (Proof shortened by Eric Schmidt, 4-Apr-2007) Reduce axiom usage. (Revised by Gino Giotto, 17-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab1v.1	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
2		opeq1	$$⊢x=z\to ⟨x,y⟩=⟨z,y⟩$$
3	2	eqeq2d	$$⊢x=z\to \left(w=⟨x,y⟩\leftrightarrow w=⟨z,y⟩\right)$$
4	3 1	anbi12d	$$⊢x=z\to \left(\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(w=⟨z,y⟩\wedge \psi \right)\right)$$
5	4	exbidv	$$⊢x=z\to \left(\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\left(w=⟨z,y⟩\wedge \psi \right)\right)$$
6	5	cbvexvw	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)$$
7	6	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\}$$
8		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{w|\exists x\exists y\left(w=⟨x,y⟩\wedge \phi \right)\right\}$$
9		df-opab	$$⊢\left\{⟨z,y⟩|\psi \right\}=\left\{w|\exists z\exists y\left(w=⟨z,y⟩\wedge \psi \right)\right\}$$
10	7 8 9	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,y⟩|\psi \right\}$$