cbvopab1davw

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

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

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

Metamath Proof Explorer