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

Proof

Step	Hyp	Ref	Expression
1		cbvoprab13vw.1	$$⊢\left(x=w\wedge z=v\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		opeq1	$$⊢x=w\to ⟨x,y⟩=⟨w,y⟩$$
3	2	adantr	$$⊢\left(x=w\wedge z=v\right)\to ⟨x,y⟩=⟨w,y⟩$$
4		simpr	$$⊢\left(x=w\wedge z=v\right)\to z=v$$
5	3 4	opeq12d	$$⊢\left(x=w\wedge z=v\right)\to ⟨⟨x,y⟩,z⟩=⟨⟨w,y⟩,v⟩$$
6	5	eqeq2d	$$⊢\left(x=w\wedge z=v\right)\to \left(t=⟨⟨x,y⟩,z⟩\leftrightarrow t=⟨⟨w,y⟩,v⟩\right)$$
7	6 1	anbi12d	$$⊢\left(x=w\wedge z=v\right)\to \left(\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \left(t=⟨⟨w,y⟩,v⟩\wedge \chi \right)\right)$$
8	7	cbvexdvaw	$$⊢x=w\to \left(\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \exists v\left(t=⟨⟨w,y⟩,v⟩\wedge \chi \right)\right)$$
9	8	exbidv	$$⊢x=w\to \left(\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \exists y\exists v\left(t=⟨⟨w,y⟩,v⟩\wedge \chi \right)\right)$$
10	9	cbvexvw	$$⊢\exists x\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\leftrightarrow \exists w\exists y\exists v\left(t=⟨⟨w,y⟩,v⟩\wedge \chi \right)$$
11	10	abbii	$$⊢\left\{t|\exists x\exists y\exists z\left(t=⟨⟨x,y⟩,z⟩\wedge \psi \right)\right\}=\left\{t|\exists w\exists y\exists v\left(t=⟨⟨w,y⟩,v⟩\wedge \chi \right)\right\}$$
12		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\}$$
13		df-oprab	$$⊢\left\{⟨⟨w,y⟩,v⟩|\chi \right\}=\left\{t|\exists w\exists y\exists v\left(t=⟨⟨w,y⟩,v⟩\wedge \chi \right)\right\}$$
14	11 12 13	3eqtr4i	$$⊢\left\{⟨⟨x,y⟩,z⟩|\psi \right\}=\left\{⟨⟨w,y⟩,v⟩|\chi \right\}$$