Theorem cbvopabdavw

Description: Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopabdavw.1	|- ( ( ( ph /\ x = z ) /\ y = w ) -> ( ps <-> ch ) )
2		simplr	|- ( ( ( ph /\ x = z ) /\ y = w ) -> x = z )
3		simpr	|- ( ( ( ph /\ x = z ) /\ y = w ) -> y = w )
4	2 3	opeq12d	|- ( ( ( ph /\ x = z ) /\ y = w ) -> <. x , y >. = <. z , w >. )
5	4	eqeq2d	|- ( ( ( ph /\ x = z ) /\ y = w ) -> ( t = <. x , y >. <-> t = <. z , w >. ) )
6	5 1	anbi12d	|- ( ( ( ph /\ x = z ) /\ y = w ) -> ( ( t = <. x , y >. /\ ps ) <-> ( t = <. z , w >. /\ ch ) ) )
7	6	cbvexdvaw	|- ( ( ph /\ x = z ) -> ( E. y ( t = <. x , y >. /\ ps ) <-> E. w ( t = <. z , w >. /\ ch ) ) )
8	7	cbvexdvaw	|- ( ph -> ( E. x E. y ( t = <. x , y >. /\ ps ) <-> E. z E. w ( t = <. z , w >. /\ ch ) ) )
9	8	abbidv	|- ( ph -> { t | E. x E. y ( t = <. x , y >. /\ ps ) } = { t | E. z E. w ( t = <. z , w >. /\ ch ) } )
10		df-opab	|- { <. x , y >. | ps } = { t | E. x E. y ( t = <. x , y >. /\ ps ) }
11		df-opab	|- { <. z , w >. | ch } = { t | E. z E. w ( t = <. z , w >. /\ ch ) }
12	9 10 11	3eqtr4g	|- ( ph -> { <. x , y >. | ps } = { <. z , w >. | ch } )