This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvopabv

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996) Reduce axiom usage. (Revised by GG, 15-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvopabv.1	$⊢ (x = z \land y = w) \to (φ \leftrightarrow ψ)$
2		opeq12	$⊢ (x = z \land y = w) \to ⟨x, y⟩ = ⟨z, w⟩$
3	2	eqeq2d	$⊢ (x = z \land y = w) \to (v = ⟨x, y⟩ \leftrightarrow v = ⟨z, w⟩)$
4	3 1	anbi12d	$⊢ (x = z \land y = w) \to ((v = ⟨x, y⟩ \land φ) \leftrightarrow (v = ⟨z, w⟩ \land ψ))$
5	4	cbvex2vw	$⊢ \exists x \exists y (v = ⟨x, y⟩ \land φ) \leftrightarrow \exists z \exists w (v = ⟨z, w⟩ \land ψ)$
6	5	abbii	$⊢ \{v \| \exists x \exists y (v = ⟨x, y⟩ \land φ)\} = \{v \| \exists z \exists w (v = ⟨z, w⟩ \land ψ)\}$
7		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{v \| \exists x \exists y (v = ⟨x, y⟩ \land φ)\}$
8		df-opab	$⊢ \{⟨z, w⟩ \| ψ\} = \{v \| \exists z \exists w (v = ⟨z, w⟩ \land ψ)\}$
9	6 7 8	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨z, w⟩ \| ψ\}$