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

Metamath Proof Explorer

Theorem moaneu

Description: Nested at-most-one and unique existential quantifiers. (Contributed by NM, 25-Jan-2006) (Proof shortened by Wolf Lammen, 27-Dec-2018)

Ref Expression
Assertion moaneu ⊢ ∃* x φ ∧ ∃! x φ

Proof

Step Hyp Ref Expression
1 moanmo ⊢ ∃* x φ ∧ ∃* x φ
2 eumo ⊢ ∃! x φ → ∃* x φ
3 2 anim2i ⊢ φ ∧ ∃! x φ → φ ∧ ∃* x φ
4 3 moimi ⊢ ∃* x φ ∧ ∃* x φ → ∃* x φ ∧ ∃! x φ
5 1 4 ax-mp ⊢ ∃* x φ ∧ ∃! x φ