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

Metamath Proof Explorer

Theorem eumoi

Description: Uniqueness inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995)

		Ref	Expression
	Hypothesis	eumoi.1	$⊢ \exists! x φ$
	Assertion	eumoi	$⊢ \exists^{*} x φ$

Step	Hyp	Ref	Expression
1		eumoi.1	$⊢ \exists! x φ$
2		eumo	$⊢ \exists! x φ \to \exists^{*} x φ$
3	1 2	ax-mp	$⊢ \exists^{*} x φ$