Theorem cbvoprab3v

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004) (Revised by David Abernethy, 19-Jun-2012)

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

Proof

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