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	|- F/ z ph
	cbvopab.2	|- F/ w ph
	cbvopab.3	|- F/ x ps
	cbvopab.4	|- F/ y ps
	cbvopab.5	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion	cbvopab	|- { <. x , y >. | ph } = { <. z , w >. | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvopab.1	|- F/ z ph
2		cbvopab.2	|- F/ w ph
3		cbvopab.3	|- F/ x ps
4		cbvopab.4	|- F/ y ps
5		cbvopab.5	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
6		nfv	|- F/ z v = <. x , y >.
7	6 1	nfan	|- F/ z ( v = <. x , y >. /\ ph )
8		nfv	|- F/ w v = <. x , y >.
9	8 2	nfan	|- F/ w ( v = <. x , y >. /\ ph )
10		nfv	|- F/ x v = <. z , w >.
11	10 3	nfan	|- F/ x ( v = <. z , w >. /\ ps )
12		nfv	|- F/ y v = <. z , w >.
13	12 4	nfan	|- F/ y ( v = <. z , w >. /\ ps )
14		opeq12	|- ( ( x = z /\ y = w ) -> <. x , y >. = <. z , w >. )
15	14	eqeq2d	|- ( ( x = z /\ y = w ) -> ( v = <. x , y >. <-> v = <. z , w >. ) )
16	15 5	anbi12d	|- ( ( x = z /\ y = w ) -> ( ( v = <. x , y >. /\ ph ) <-> ( v = <. z , w >. /\ ps ) ) )
17	7 9 11 13 16	cbvex2v	|- ( E. x E. y ( v = <. x , y >. /\ ph ) <-> E. z E. w ( v = <. z , w >. /\ ps ) )
18	17	abbii	|- { v | E. x E. y ( v = <. x , y >. /\ ph ) } = { v | E. z E. w ( v = <. z , w >. /\ ps ) }
19		df-opab	|- { <. x , y >. | ph } = { v | E. x E. y ( v = <. x , y >. /\ ph ) }
20		df-opab	|- { <. z , w >. | ps } = { v | E. z E. w ( v = <. z , w >. /\ ps ) }
21	18 19 20	3eqtr4i	|- { <. x , y >. | ph } = { <. z , w >. | ps }