Metamath Proof Explorer

Theorem cbvoprab23vw

Description: Change the second and third bound variables in an operation abstraction, using implicit substitution. (Contributed by GG, 14-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 cbvoprab23vw.1 
 |-  ( ( y = w /\ z = v ) -> ( ps <-> ch ) )
2 opeq2 
 |-  ( y = w -> <. x , y >. = <. x , w >. )
3 2 adantr 
 |-  ( ( y = w /\ z = v ) -> <. x , y >. = <. x , w >. )
4 simpr 
 |-  ( ( y = w /\ z = v ) -> z = v )
5 3 4 opeq12d 
 |-  ( ( y = w /\ z = v ) -> <. <. x , y >. , z >. = <. <. x , w >. , v >. )
6 5 eqeq2d 
 |-  ( ( y = w /\ z = v ) -> ( t = <. <. x , y >. , z >. <-> t = <. <. x , w >. , v >. ) )
7 6 1 anbi12d 
 |-  ( ( y = w /\ z = v ) -> ( ( t = <. <. x , y >. , z >. /\ ps ) <-> ( t = <. <. x , w >. , v >. /\ ch ) ) )
8 7 cbvex2vw 
 |-  ( E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. w E. v ( t = <. <. x , w >. , v >. /\ ch ) )
9 8 exbii 
 |-  ( E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. x E. w E. v ( t = <. <. x , w >. , v >. /\ ch ) )
10 9 abbii 
 |-  { t | E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) } = { t | E. x E. w E. v ( t = <. <. x , w >. , v >. /\ ch ) }
11 df-oprab 
 |-  { <. <. x , y >. , z >. | ps } = { t | E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) }
12 df-oprab 
 |-  { <. <. x , w >. , v >. | ch } = { t | E. x E. w E. v ( t = <. <. x , w >. , v >. /\ ch ) }
13 10 11 12 3eqtr4i 
 |-  { <. <. x , y >. , z >. | ps } = { <. <. x , w >. , v >. | ch }