Metamath Proof Explorer

Theorem cbvoprab123davw

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

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

Proof

Step Hyp Ref Expression
1 cbvoprab123davw.1 
 |-  ( ( ( ( ph /\ x = w ) /\ y = u ) /\ z = v ) -> ( ps <-> ch ) )
2 simplr 
 |-  ( ( ( ph /\ x = w ) /\ y = u ) -> x = w )
3 simpr 
 |-  ( ( ( ph /\ x = w ) /\ y = u ) -> y = u )
4 2 3 opeq12d 
 |-  ( ( ( ph /\ x = w ) /\ y = u ) -> <. x , y >. = <. w , u >. )
5 4 adantr 
 |-  ( ( ( ( ph /\ x = w ) /\ y = u ) /\ z = v ) -> <. x , y >. = <. w , u >. )
6 simpr 
 |-  ( ( ( ( ph /\ x = w ) /\ y = u ) /\ z = v ) -> z = v )
7 5 6 opeq12d 
 |-  ( ( ( ( ph /\ x = w ) /\ y = u ) /\ z = v ) -> <. <. x , y >. , z >. = <. <. w , u >. , v >. )
8 7 eqeq2d 
 |-  ( ( ( ( ph /\ x = w ) /\ y = u ) /\ z = v ) -> ( t = <. <. x , y >. , z >. <-> t = <. <. w , u >. , v >. ) )
9 8 1 anbi12d 
 |-  ( ( ( ( ph /\ x = w ) /\ y = u ) /\ z = v ) -> ( ( t = <. <. x , y >. , z >. /\ ps ) <-> ( t = <. <. w , u >. , v >. /\ ch ) ) )
10 9 cbvexdvaw 
 |-  ( ( ( ph /\ x = w ) /\ y = u ) -> ( E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. v ( t = <. <. w , u >. , v >. /\ ch ) ) )
11 10 cbvexdvaw 
 |-  ( ( ph /\ x = w ) -> ( E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. u E. v ( t = <. <. w , u >. , v >. /\ ch ) ) )
12 11 cbvexdvaw 
 |-  ( ph -> ( E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. w E. u E. v ( t = <. <. w , u >. , v >. /\ ch ) ) )
13 12 abbidv 
 |-  ( ph -> { t | E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) } = { t | E. w E. u E. v ( t = <. <. w , u >. , v >. /\ ch ) } )
14 df-oprab 
 |-  { <. <. x , y >. , z >. | ps } = { t | E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) }
15 df-oprab 
 |-  { <. <. w , u >. , v >. | ch } = { t | E. w E. u E. v ( t = <. <. w , u >. , v >. /\ ch ) }
16 13 14 15 3eqtr4g 
 |-  ( ph -> { <. <. x , y >. , z >. | ps } = { <. <. w , u >. , v >. | ch } )