Theorem cbvoprab1davw

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

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

Proof

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