Theorem eumoi

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

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

Proof

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