Theorem cbvoprab1

Description: Rule used to change first bound variable in an operation abstraction, using implicit substitution. (Contributed by NM, 20-Dec-2008) (Revised by Mario Carneiro, 5-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab1.1	$$⊢Ⅎw\phi$$
2		cbvoprab1.2	$$⊢Ⅎx\psi$$
3		cbvoprab1.3	$$⊢x=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		nfv	$$⊢Ⅎxv=⟨w,y⟩$$
8	7 2	nfan	$$⊢Ⅎx\left(v=⟨w,y⟩\wedge \psi \right)$$
9	8	nfex	$$⊢Ⅎx\exists y\left(v=⟨w,y⟩\wedge \psi \right)$$
10		opeq1	$$⊢x=w\to ⟨x,y⟩=⟨w,y⟩$$
11	10	eqeq2d	$$⊢x=w\to \left(v=⟨x,y⟩\leftrightarrow v=⟨w,y⟩\right)$$
12	11 3	anbi12d	$$⊢x=w\to \left(\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(v=⟨w,y⟩\wedge \psi \right)\right)$$
13	12	exbidv	$$⊢x=w\to \left(\exists y\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists y\left(v=⟨w,y⟩\wedge \psi \right)\right)$$
14	6 9 13	cbvexv1	$$⊢\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists w\exists y\left(v=⟨w,y⟩\wedge \psi \right)$$
15	14	opabbii	$$⊢\left\{⟨v,z⟩|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}=\left\{⟨v,z⟩|\exists w\exists y\left(v=⟨w,y⟩\wedge \psi \right)\right\}$$
16		dfoprab2	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨v,z⟩|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}$$
17		dfoprab2	$$⊢\left\{⟨⟨w,y⟩,z⟩|\psi \right\}=\left\{⟨v,z⟩|\exists w\exists y\left(v=⟨w,y⟩\wedge \psi \right)\right\}$$
18	15 16 17	3eqtr4i	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨w,y⟩,z⟩|\psi \right\}$$