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	$$⊢{\exists }^{*}x\phi \to \left\{x|\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-mo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$
2		df-sn	$$⊢\left\{y\right\}=\left\{x|x=y\right\}$$
3		vsnex	$$⊢\left\{y\right\}\in \mathrm{V}$$
4	2 3	eqeltrri	$$⊢\left\{x|x=y\right\}\in \mathrm{V}$$
5	4	a1i	$$⊢\forall x\left(\phi \to x=y\right)\to \left\{x|x=y\right\}\in \mathrm{V}$$
6		ss2abim	$$⊢\forall x\left(\phi \to x=y\right)\to \left\{x|\phi \right\}\subseteq \left\{x|x=y\right\}$$
7	5 6	ssexd	$$⊢\forall x\left(\phi \to x=y\right)\to \left\{x|\phi \right\}\in \mathrm{V}$$
8	7	exlimiv	$$⊢\exists y\forall x\left(\phi \to x=y\right)\to \left\{x|\phi \right\}\in \mathrm{V}$$
9	1 8	sylbi	$$⊢{\exists }^{*}x\phi \to \left\{x|\phi \right\}\in \mathrm{V}$$