cbvoprab123vw

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

		Ref	Expression
	Hypothesis	cbvoprab123vw.1	$⊢ ((x = w \land y = u) \land z = v) \to (ψ \leftrightarrow χ)$
	Assertion	cbvoprab123vw	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨⟨w, u⟩, v⟩ \| χ\}$

Step	Hyp	Ref	Expression
1		cbvoprab123vw.1	$⊢ ((x = w \land y = u) \land z = v) \to (ψ \leftrightarrow χ)$
2		simpll	$⊢ ((x = w \land y = u) \land z = v) \to x = w$
3		simplr	$⊢ ((x = w \land y = u) \land z = v) \to y = u$
4	2 3	opeq12d	$⊢ ((x = w \land y = u) \land z = v) \to ⟨x, y⟩ = ⟨w, u⟩$
5		simpr	$⊢ ((x = w \land y = u) \land z = v) \to z = v$
6	4 5	opeq12d	$⊢ ((x = w \land y = u) \land z = v) \to ⟨⟨x, y⟩, z⟩ = ⟨⟨w, u⟩, v⟩$
7	6	eqeq2d	$⊢ ((x = w \land y = u) \land z = v) \to (t = ⟨⟨x, y⟩, z⟩ \leftrightarrow t = ⟨⟨w, u⟩, v⟩)$
8	7 1	anbi12d	$⊢ ((x = w \land y = u) \land z = v) \to ((t = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow (t = ⟨⟨w, u⟩, v⟩ \land χ))$
9	8	cbvexdvaw	$⊢ (x = w \land y = u) \to (\exists z (t = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow \exists v (t = ⟨⟨w, u⟩, v⟩ \land χ))$
10	9	cbvex2vw	$⊢ \exists x \exists y \exists z (t = ⟨⟨x, y⟩, z⟩ \land ψ) \leftrightarrow \exists w \exists u \exists v (t = ⟨⟨w, u⟩, v⟩ \land χ)$
11	10	abbii	$⊢ \{t \| \exists x \exists y \exists z (t = ⟨⟨x, y⟩, z⟩ \land ψ)\} = \{t \| \exists w \exists u \exists v (t = ⟨⟨w, u⟩, v⟩ \land χ)\}$
12		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{t \| \exists x \exists y \exists z (t = ⟨⟨x, y⟩, z⟩ \land ψ)\}$
13		df-oprab	$⊢ \{⟨⟨w, u⟩, v⟩ \| χ\} = \{t \| \exists w \exists u \exists v (t = ⟨⟨w, u⟩, v⟩ \land χ)\}$
14	11 12 13	3eqtr4i	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨⟨w, u⟩, v⟩ \| χ\}$

Metamath Proof Explorer