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

Metamath Proof Explorer

Theorem euim

Description: Add unique existential quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005) (Proof shortened by Andrew Salmon, 14-Jun-2011) (Proof shortened by Wolf Lammen, 1-Oct-2023)

Ref Expression
Assertion euim ⊢ ∃ x φ ∧ ∀ x φ → ψ → ∃! x ψ → ∃! x φ

Proof

Step Hyp Ref Expression
1 euimmo ⊢ ∀ x φ → ψ → ∃! x ψ → ∃* x φ
2 exmoeub ⊢ ∃ x φ → ∃* x φ ↔ ∃! x φ
3 2 biimpd ⊢ ∃ x φ → ∃* x φ → ∃! x φ
4 1 3 sylan9r ⊢ ∃ x φ ∧ ∀ x φ → ψ → ∃! x ψ → ∃! x φ