Theorem cbvopab

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 14-Sep-2003)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopab.1	$$⊢Ⅎz\phi$$
2		cbvopab.2	$$⊢Ⅎw\phi$$
3		cbvopab.3	$$⊢Ⅎx\psi$$
4		cbvopab.4	$$⊢Ⅎy\psi$$
5		cbvopab.5	$$⊢\left(x=z\wedge y=w\right)\to \left(\phi \leftrightarrow \psi \right)$$
6		nfv	$$⊢Ⅎzv=⟨x,y⟩$$
7	6 1	nfan	$$⊢Ⅎz\left(v=⟨x,y⟩\wedge \phi \right)$$
8		nfv	$$⊢Ⅎwv=⟨x,y⟩$$
9	8 2	nfan	$$⊢Ⅎw\left(v=⟨x,y⟩\wedge \phi \right)$$
10		nfv	$$⊢Ⅎxv=⟨z,w⟩$$
11	10 3	nfan	$$⊢Ⅎx\left(v=⟨z,w⟩\wedge \psi \right)$$
12		nfv	$$⊢Ⅎyv=⟨z,w⟩$$
13	12 4	nfan	$$⊢Ⅎy\left(v=⟨z,w⟩\wedge \psi \right)$$
14		opeq12	$$⊢\left(x=z\wedge y=w\right)\to ⟨x,y⟩=⟨z,w⟩$$
15	14	eqeq2d	$$⊢\left(x=z\wedge y=w\right)\to \left(v=⟨x,y⟩\leftrightarrow v=⟨z,w⟩\right)$$
16	15 5	anbi12d	$$⊢\left(x=z\wedge y=w\right)\to \left(\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \left(v=⟨z,w⟩\wedge \psi \right)\right)$$
17	7 9 11 13 16	cbvex2v	$$⊢\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\leftrightarrow \exists z\exists w\left(v=⟨z,w⟩\wedge \psi \right)$$
18	17	abbii	$$⊢\left\{v|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}=\left\{v|\exists z\exists w\left(v=⟨z,w⟩\wedge \psi \right)\right\}$$
19		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{v|\exists x\exists y\left(v=⟨x,y⟩\wedge \phi \right)\right\}$$
20		df-opab	$$⊢\left\{⟨z,w⟩|\psi \right\}=\left\{v|\exists z\exists w\left(v=⟨z,w⟩\wedge \psi \right)\right\}$$
21	18 19 20	3eqtr4i	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨z,w⟩|\psi \right\}$$