Theorem cbvopab2v

Description: Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999)

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

Proof

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