Theorem cbvopab2

Description: Change second bound variable in an ordered-pair class abstraction, using explicit substitution. (Contributed by NM, 22-Aug-2013)

	Ref	Expression
Hypotheses	cbvopab2.1	|- F/ z ph
	cbvopab2.2	|- F/ y ps
	cbvopab2.3	|- ( y = z -> ( ph <-> ps ) )
Assertion	cbvopab2	|- { <. x , y >. | ph } = { <. x , z >. | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvopab2.1	|- F/ z ph
2		cbvopab2.2	|- F/ y ps
3		cbvopab2.3	|- ( y = z -> ( ph <-> ps ) )
4		nfv	|- F/ z w = <. x , y >.
5	4 1	nfan	|- F/ z ( w = <. x , y >. /\ ph )
6		nfv	|- F/ y w = <. x , z >.
7	6 2	nfan	|- F/ y ( w = <. x , z >. /\ ps )
8		opeq2	|- ( y = z -> <. x , y >. = <. x , z >. )
9	8	eqeq2d	|- ( y = z -> ( w = <. x , y >. <-> w = <. x , z >. ) )
10	9 3	anbi12d	|- ( y = z -> ( ( w = <. x , y >. /\ ph ) <-> ( w = <. x , z >. /\ ps ) ) )
11	5 7 10	cbvexv1	|- ( E. y ( w = <. x , y >. /\ ph ) <-> E. z ( w = <. x , z >. /\ ps ) )
12	11	exbii	|- ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. x E. z ( w = <. x , z >. /\ ps ) )
13	12	abbii	|- { w | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. x E. z ( w = <. x , z >. /\ ps ) }
14		df-opab	|- { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) }
15		df-opab	|- { <. x , z >. | ps } = { w | E. x E. z ( w = <. x , z >. /\ ps ) }
16	13 14 15	3eqtr4i	|- { <. x , y >. | ph } = { <. x , z >. | ps }