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

Metamath Proof Explorer

Theorem moeu

Description: Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995) This used to be the definition of the at-most-one quantifier, while df-mo was then proved as dfmo . (Revised by BJ, 30-Sep-2022)

Ref Expression
Assertion moeu ⊢ ∃* x φ ↔ ∃ x φ → ∃! x φ

Proof

Step Hyp Ref Expression
1 moabs ⊢ ∃* x φ ↔ ∃ x φ → ∃* x φ
2 exmoeub ⊢ ∃ x φ → ∃* x φ ↔ ∃! x φ
3 2 pm5.74i ⊢ ∃ x φ → ∃* x φ ↔ ∃ x φ → ∃! x φ
4 1 3 bitri ⊢ ∃* x φ ↔ ∃ x φ → ∃! x φ