Theorem cbvoprab12

Description: Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 21-Feb-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab12.1	$$⊢Ⅎw\phi$$
2		cbvoprab12.2	$$⊢Ⅎv\phi$$
3		cbvoprab12.3	$$⊢Ⅎx\psi$$
4		cbvoprab12.4	$$⊢Ⅎy\psi$$
5		cbvoprab12.5	$$⊢\left(x=w\wedge y=v\right)\to \left(\phi \leftrightarrow \psi \right)$$
6		nfv	$$⊢Ⅎwu=⟨x,y⟩$$
7	6 1	nfan	$$⊢Ⅎw\left(u=⟨x,y⟩\wedge \phi \right)$$
8		nfv	$$⊢Ⅎvu=⟨x,y⟩$$
9	8 2	nfan	$$⊢Ⅎv\left(u=⟨x,y⟩\wedge \phi \right)$$
10		nfv	$$⊢Ⅎxu=⟨w,v⟩$$
11	10 3	nfan	$$⊢Ⅎx\left(u=⟨w,v⟩\wedge \psi \right)$$
12		nfv	$$⊢Ⅎyu=⟨w,v⟩$$
13	12 4	nfan	$$⊢Ⅎy\left(u=⟨w,v⟩\wedge \psi \right)$$
14		opeq12	$$⊢\left(x=w\wedge y=v\right)\to ⟨x,y⟩=⟨w,v⟩$$
15	14	eqeq2d	$$⊢\left(x=w\wedge y=v\right)\to \left(u=⟨x,y⟩\leftrightarrow u=⟨w,v⟩\right)$$
16	15 5	anbi12d	$$⊢\left(x=w\wedge y=v\right)\to \left(\left(u=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(u=⟨w,v⟩\wedge \psi \right)\right)$$
17	7 9 11 13 16	cbvex2v	$$⊢\exists x\exists y\left(u=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists w\exists v\left(u=⟨w,v⟩\wedge \psi \right)$$
18	17	opabbii	$$⊢\left\{⟨u,z⟩|\exists x\exists y\left(u=⟨x,y⟩\wedge \phi \right)\right\}=\left\{⟨u,z⟩|\exists w\exists v\left(u=⟨w,v⟩\wedge \psi \right)\right\}$$
19		dfoprab2	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨u,z⟩|\exists x\exists y\left(u=⟨x,y⟩\wedge \phi \right)\right\}$$
20		dfoprab2	$$⊢\left\{⟨⟨w,v⟩,z⟩|\psi \right\}=\left\{⟨u,z⟩|\exists w\exists v\left(u=⟨w,v⟩\wedge \psi \right)\right\}$$
21	18 19 20	3eqtr4i	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨w,v⟩,z⟩|\psi \right\}$$