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

Metamath Proof Explorer

Theorem exmoeu

Description: Existence is equivalent to uniqueness implying existential uniqueness. (Contributed by NM, 5-Apr-2004) (Proof shortened by Wolf Lammen, 5-Dec-2018) (Proof shortened by BJ, 7-Oct-2022)

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

Proof

Step	Hyp	Ref	Expression
1		exmoeub	$⊢ \exists x φ \to (\exists^{*} x φ \leftrightarrow \exists! x φ)$
2	1	biimpd	$⊢ \exists x φ \to (\exists^{*} x φ \to \exists! x φ)$
3		nexmo	$⊢ \neg \exists x φ \to \exists^{*} x φ$
4	3	con1i	$⊢ \neg \exists^{*} x φ \to \exists x φ$
5		euex	$⊢ \exists! x φ \to \exists x φ$
6	4 5	ja	$⊢ (\exists^{*} x φ \to \exists! x φ) \to \exists x φ$
7	2 6	impbii	$⊢ \exists x φ \leftrightarrow (\exists^{*} x φ \to \exists! x φ)$