cbvoprab3davw

Description: Change the third bound variable in an operation abstraction. Deduction form. (Contributed by GG, 14-Aug-2025)

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

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

Metamath Proof Explorer