Theorem moeu2

Description: Uniqueness is equivalent to non-existence or unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by Peter Mazsa, 19-Nov-2024)

	Ref	Expression
Assertion	moeu2	⊢ ( ∃* 𝑥 𝜑 ↔ ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		moeu	⊢ ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
2		imor	⊢ ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) )
3	1 2	bitri	⊢ ( ∃* 𝑥 𝜑 ↔ ( ¬ ∃ 𝑥 𝜑 ∨ ∃! 𝑥 𝜑 ) )