Theorem cbvoprab3

Description: Rule used to change the third bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 22-Aug-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab3.1	$$⊢Ⅎw\phi$$
2		cbvoprab3.2	$$⊢Ⅎz\psi$$
3		cbvoprab3.3	$$⊢z=w\to \left(\phi \leftrightarrow \psi \right)$$
4		nfv	$$⊢Ⅎwv=⟨x,y⟩$$
5	4 1	nfan	$$⊢Ⅎw\left(v=⟨x,y⟩\wedge \phi \right)$$
6	5	nfex	$$⊢Ⅎw\exists y\left(v=⟨x,y⟩\wedge \phi \right)$$
7	6	nfex	$$⊢Ⅎw\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)$$
8		nfv	$$⊢Ⅎzv=⟨x,y⟩$$
9	8 2	nfan	$$⊢Ⅎz\left(v=⟨x,y⟩\wedge \psi \right)$$
10	9	nfex	$$⊢Ⅎz\exists y\left(v=⟨x,y⟩\wedge \psi \right)$$
11	10	nfex	$$⊢Ⅎz\exists x\exists y\left(v=⟨x,y⟩\wedge \psi \right)$$
12	3	anbi2d	$$⊢z=w\to \left(\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(v=⟨x,y⟩\wedge \psi \right)\right)$$
13	12	2exbidv	$$⊢z=w\to \left(\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(v=⟨x,y⟩\wedge \psi \right)\right)$$
14	7 11 13	cbvopab2	$$⊢\left\{⟨v,z⟩|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}=\left\{⟨v,w⟩|\exists x\exists y\left(v=⟨x,y⟩\wedge \psi \right)\right\}$$
15		dfoprab2	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨v,z⟩|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}$$
16		dfoprab2	$$⊢\left\{⟨⟨x,y⟩,w⟩|\psi \right\}=\left\{⟨v,w⟩|\exists x\exists y\left(v=⟨x,y⟩\wedge \psi \right)\right\}$$
17	14 15 16	3eqtr4i	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨x,y⟩,w⟩|\psi \right\}$$