Theorem cbvopab2davw

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

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

Proof

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