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

Metamath Proof Explorer

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 ⊢ ∃* x φ ↔ ¬ ∃ x φ ∨ ∃! x φ

Proof

Step Hyp Ref Expression
1 moeu ⊢ ∃* x φ ↔ ∃ x φ → ∃! x φ
2 imor ⊢ ∃ x φ → ∃! x φ ↔ ¬ ∃ x φ ∨ ∃! x φ
3 1 2 bitri ⊢ ∃* x φ ↔ ¬ ∃ x φ ∨ ∃! x φ