Theorem cbvopab1davw

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

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

Proof

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