cbvopabdavw

Description: Change bound variables in an ordered-pair class abstraction. Deduction form. (Contributed by GG, 14-Aug-2025)

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

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

Metamath Proof Explorer