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

Metamath Proof Explorer

Theorem moabex

Description: "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996) Avoid axioms. (Revised by SN, 2-Feb-2026)

Ref Expression
Assertion moabex ⊢ ∃* x φ → x | φ ∈ V

Proof

Step Hyp Ref Expression
1 df-mo ⊢ ∃* x φ ↔ ∃ y ∀ x φ → x = y
2 df-sn ⊢ y = x | x = y
3 vsnex ⊢ y ∈ V
4 2 3 eqeltrri ⊢ x | x = y ∈ V
5 4 a1i ⊢ ∀ x φ → x = y → x | x = y ∈ V
6 ss2abim ⊢ ∀ x φ → x = y → x | φ ⊆ x | x = y
7 5 6 ssexd ⊢ ∀ x φ → x = y → x | φ ∈ V
8 7 exlimiv ⊢ ∃ y ∀ x φ → x = y → x | φ ∈ V
9 1 8 sylbi ⊢ ∃* x φ → x | φ ∈ V