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

Metamath Proof Explorer

Theorem opabbid

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 21-Feb-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011)

		Ref	Expression
	Hypotheses	opabbid.1	$⊢ Ⅎ x φ$
		opabbid.2	$⊢ Ⅎ y φ$
		opabbid.3	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	opabbid	$⊢ φ \to \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| χ\}$

Proof

Step	Hyp	Ref	Expression
1		opabbid.1	$⊢ Ⅎ x φ$
2		opabbid.2	$⊢ Ⅎ y φ$
3		opabbid.3	$⊢ φ \to (ψ \leftrightarrow χ)$
4	3	anbi2d	$⊢ φ \to ((z = ⟨x, y⟩ \land ψ) \leftrightarrow (z = ⟨x, y⟩ \land χ))$
5	2 4	exbid	$⊢ φ \to (\exists y (z = ⟨x, y⟩ \land ψ) \leftrightarrow \exists y (z = ⟨x, y⟩ \land χ))$
6	1 5	exbid	$⊢ φ \to (\exists x \exists y (z = ⟨x, y⟩ \land ψ) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land χ))$
7	6	abbidv	$⊢ φ \to \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land χ)\}$
8		df-opab	$⊢ \{⟨x, y⟩ \| ψ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land ψ)\}$
9		df-opab	$⊢ \{⟨x, y⟩ \| χ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land χ)\}$
10	7 8 9	3eqtr4g	$⊢ φ \to \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| χ\}$