Metamath Proof Explorer

Theorem cbvoprab3davw

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

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

Proof

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