Theorem cbvopab1v

Description: Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution. (Contributed by NM, 31-Jul-2003) (Proof shortened by Eric Schmidt, 4-Apr-2007) Reduce axiom usage. (Revised by Gino Giotto, 17-Nov-2024)

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

Proof

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