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	|- ( E* x ph -> { x | ph } e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-mo	|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
2		df-sn	|- { y } = { x | x = y }
3		vsnex	|- { y } e. _V
4	2 3	eqeltrri	|- { x | x = y } e. _V
5	4	a1i	|- ( A. x ( ph -> x = y ) -> { x | x = y } e. _V )
6		ss2abim	|- ( A. x ( ph -> x = y ) -> { x | ph } C_ { x | x = y } )
7	5 6	ssexd	|- ( A. x ( ph -> x = y ) -> { x | ph } e. _V )
8	7	exlimiv	|- ( E. y A. x ( ph -> x = y ) -> { x | ph } e. _V )
9	1 8	sylbi	|- ( E* x ph -> { x | ph } e. _V )