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

Metamath Proof Explorer

Theorem euimmo

Description: Existential uniqueness implies uniqueness through reverse implication. (Contributed by NM, 22-Apr-1995)

Ref Expression
Assertion euimmo ⊢ ∀ x φ → ψ → ∃! x ψ → ∃* x φ

Proof

Step Hyp Ref Expression
1 eumo ⊢ ∃! x ψ → ∃* x ψ
2 moim ⊢ ∀ x φ → ψ → ∃* x ψ → ∃* x φ
3 1 2 syl5 ⊢ ∀ x φ → ψ → ∃! x ψ → ∃* x φ