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

Metamath Proof Explorer

Theorem exmoeub

Description: Existence implies that uniqueness is equivalent to unique existence. (Contributed by NM, 5-Apr-2004)

		Ref	Expression
	Assertion	exmoeub	$⊢ \exists x φ \to (\exists^{*} x φ \leftrightarrow \exists! x φ)$

Step	Hyp	Ref	Expression
1		df-eu	$⊢ \exists! x φ \leftrightarrow (\exists x φ \land \exists^{*} x φ)$
2	1	baibr	$⊢ \exists x φ \to (\exists^{*} x φ \leftrightarrow \exists! x φ)$