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	⊢ ( ∃* 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
2		df-sn	⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 }
3		vsnex	⊢ { 𝑦 } ∈ V
4	2 3	eqeltrri	⊢ { 𝑥 ∣ 𝑥 = 𝑦 } ∈ V
5	4	a1i	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝑥 = 𝑦 } ∈ V )
6		ss2abim	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝑥 = 𝑦 } )
7	5 6	ssexd	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ∈ V )
8	7	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ∈ V )
9	1 8	sylbi	⊢ ( ∃* 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } ∈ V )