Theorem cbvoprab13vw

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

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

Proof

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