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	$$⊢\left(y=w\wedge z=v\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	cbvoprab23vw	$$⊢\left\{⟨⟨x,y⟩,z⟩|\psi \right\}=\left\{⟨⟨x,w⟩,v⟩|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvoprab23vw.1	$$⊢\left(y=w\wedge z=v\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		opeq2	$$⊢y=w\to ⟨x,y⟩=⟨x,w⟩$$
3	2	adantr	$$⊢\left(y=w\wedge z=v\right)\to ⟨x,y⟩=⟨x,w⟩$$
4		simpr	$$⊢\left(y=w\wedge z=v\right)\to z=v$$
5	3 4	opeq12d	$$⊢\left(y=w\wedge z=v\right)\to ⟨⟨x,y⟩,z⟩=⟨⟨x,w⟩,v⟩$$
6	5	eqeq2d	$$⊢\left(y=w\wedge z=v\right)\to \left(t=⟨⟨x,y⟩,z⟩\leftrightarrow t=⟨⟨x,w⟩,v⟩\right)$$
7	6 1	anbi12d	$$⊢\left(y=w\wedge z=v\right)\to \left(\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \left(t=⟨⟨x,w⟩,v⟩\wedge \chi \right)\right)$$
8	7	cbvex2vw	$$⊢\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \exists w\exists v\left(t=⟨⟨x,w⟩,v⟩\wedge \chi \right)$$
9	8	exbii	$$⊢\exists x\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \exists x\exists w\exists v\left(t=⟨⟨x,w⟩,v⟩\wedge \chi \right)$$
10	9	abbii	$$⊢\left\{t|\exists x\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\right\}=\left\{t|\exists x\exists w\exists v\left(t=⟨⟨x,w⟩,v⟩\wedge \chi \right)\right\}$$
11		df-oprab	$$⊢\left\{⟨⟨x,y⟩,z⟩|\psi \right\}=\left\{t|\exists x\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\right\}$$
12		df-oprab	$$⊢\left\{⟨⟨x,w⟩,v⟩|\chi \right\}=\left\{t|\exists x\exists w\exists v\left(t=⟨⟨x,w⟩,v⟩\wedge \chi \right)\right\}$$
13	10 11 12	3eqtr4i	$$⊢\left\{⟨⟨x,y⟩,z⟩|\psi \right\}=\left\{⟨⟨x,w⟩,v⟩|\chi \right\}$$