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	⊢ ( ∃ 𝑥 𝜑 ↔ ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		exmoeub	⊢ ( ∃ 𝑥 𝜑 → ( ∃* 𝑥 𝜑 ↔ ∃! 𝑥 𝜑 ) )
2	1	biimpd	⊢ ( ∃ 𝑥 𝜑 → ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
3		nexmo	⊢ ( ¬ ∃ 𝑥 𝜑 → ∃* 𝑥 𝜑 )
4	3	con1i	⊢ ( ¬ ∃* 𝑥 𝜑 → ∃ 𝑥 𝜑 )
5		euex	⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑥 𝜑 )
6	4 5	ja	⊢ ( ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) → ∃ 𝑥 𝜑 )
7	2 6	impbii	⊢ ( ∃ 𝑥 𝜑 ↔ ( ∃* 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )