This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvopabv

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

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

Proof

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