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 GG, 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 }

Metamath Proof Explorer

Theorem cbvopab1v

Proof