Theorem moabex

Description: "At most one" existence implies a class abstraction exists. (Contributed by NM, 30-Dec-1996)

	Ref	Expression
Assertion	moabex	⊢ ( ∃* 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-mo	⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
2		abss	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 → 𝑥 ∈ { 𝑦 } ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝑦 } ↔ 𝑥 = 𝑦 )
4	3	imbi2i	⊢ ( ( 𝜑 → 𝑥 ∈ { 𝑦 } ) ↔ ( 𝜑 → 𝑥 = 𝑦 ) )
5	4	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 ∈ { 𝑦 } ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
6	2 5	bitri	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) )
7		snex	⊢ { 𝑦 } ∈ V
8	7	ssex	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑦 } → { 𝑥 ∣ 𝜑 } ∈ V )
9	6 8	sylbir	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ∈ V )
10	9	exlimiv	⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } ∈ V )
11	1 10	sylbi	⊢ ( ∃* 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } ∈ V )