Metamath Proof Explorer

Theorem cbvoprab12davw

Description: Change the first and second bound variables in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025)

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

Proof

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