Metamath Proof Explorer

Theorem cbvoprab1vw

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

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

Proof

Step Hyp Ref Expression
1 cbvoprab1vw.1 
 |-  ( x = w -> ( ps <-> ch ) )
2 opeq1 
 |-  ( x = w -> <. x , y >. = <. w , y >. )
3 2 opeq1d 
 |-  ( x = w -> <. <. x , y >. , z >. = <. <. w , y >. , z >. )
4 3 eqeq2d 
 |-  ( x = w -> ( t = <. <. x , y >. , z >. <-> t = <. <. w , y >. , z >. ) )
5 4 1 anbi12d 
 |-  ( x = w -> ( ( t = <. <. x , y >. , z >. /\ ps ) <-> ( t = <. <. w , y >. , z >. /\ ch ) ) )
6 5 2exbidv 
 |-  ( x = w -> ( E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. y E. z ( t = <. <. w , y >. , z >. /\ ch ) ) )
7 6 cbvexvw 
 |-  ( E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) <-> E. w E. y E. z ( t = <. <. w , y >. , z >. /\ ch ) )
8 7 abbii 
 |-  { t | E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) } = { t | E. w E. y E. z ( t = <. <. w , y >. , z >. /\ ch ) }
9 df-oprab 
 |-  { <. <. x , y >. , z >. | ps } = { t | E. x E. y E. z ( t = <. <. x , y >. , z >. /\ ps ) }
10 df-oprab 
 |-  { <. <. w , y >. , z >. | ch } = { t | E. w E. y E. z ( t = <. <. w , y >. , z >. /\ ch ) }
11 8 9 10 3eqtr4i 
 |-  { <. <. x , y >. , z >. | ps } = { <. <. w , y >. , z >. | ch }