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	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\neg \exists x\phi \vee \exists !x\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		moeu	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\exists x\phi \to \exists !x\phi \right)$$
2		imor	$$⊢\left(\exists x\phi \to \exists !x\phi \right)\leftrightarrow \left(\neg \exists x\phi \vee \exists !x\phi \right)$$
3	1 2	bitri	$$⊢{\exists }^{*}x\phi \leftrightarrow \left(\neg \exists x\phi \vee \exists !x\phi \right)$$