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 Gino Giotto, 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 }