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

Metamath Proof Explorer

Theorem moabs

Description: Absorption of existence condition by uniqueness. (Contributed by NM, 4-Nov-2002) Shorten proof and avoid df-eu . (Revised by BJ, 14-Oct-2022)

Ref Expression
Assertion moabs ⊢ ∃* x φ ↔ ∃ x φ → ∃* x φ

Proof

Step Hyp Ref Expression
1 ax-1 ⊢ ∃* x φ → ∃ x φ → ∃* x φ
2 nexmo ⊢ ¬ ∃ x φ → ∃* x φ
3 id ⊢ ∃* x φ → ∃* x φ
4 2 3 ja ⊢ ∃ x φ → ∃* x φ → ∃* x φ
5 1 4 impbii ⊢ ∃* x φ ↔ ∃ x φ → ∃* x φ