Theorem cbvopab2v

Description: Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 2-Sep-1999)

	Ref	Expression
Hypothesis	cbvopab2v.1	|- ( y = z -> ( ph <-> ps ) )
Assertion	cbvopab2v	|- { <. x , y >. | ph } = { <. x , z >. | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvopab2v.1	|- ( y = z -> ( ph <-> ps ) )
2		opeq2	|- ( y = z -> <. x , y >. = <. x , z >. )
3	2	eqeq2d	|- ( y = z -> ( w = <. x , y >. <-> w = <. x , z >. ) )
4	3 1	anbi12d	|- ( y = z -> ( ( w = <. x , y >. /\ ph ) <-> ( w = <. x , z >. /\ ps ) ) )
5	4	cbvexvw	|- ( E. y ( w = <. x , y >. /\ ph ) <-> E. z ( w = <. x , z >. /\ ps ) )
6	5	exbii	|- ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. x E. z ( w = <. x , z >. /\ ps ) )
7	6	abbii	|- { w | E. x E. y ( w = <. x , y >. /\ ph ) } = { w | E. x E. z ( w = <. x , z >. /\ ps ) }
8		df-opab	|- { <. x , y >. | ph } = { w | E. x E. y ( w = <. x , y >. /\ ph ) }
9		df-opab	|- { <. x , z >. | ps } = { w | E. x E. z ( w = <. x , z >. /\ ps ) }
10	7 8 9	3eqtr4i	|- { <. x , y >. | ph } = { <. x , z >. | ps }