Theorem moabex

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

	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		abss	|- ( { x | ph } C_ { y } <-> A. x ( ph -> x e. { y } ) )
3		velsn	|- ( x e. { y } <-> x = y )
4	3	imbi2i	|- ( ( ph -> x e. { y } ) <-> ( ph -> x = y ) )
5	4	albii	|- ( A. x ( ph -> x e. { y } ) <-> A. x ( ph -> x = y ) )
6	2 5	bitri	|- ( { x | ph } C_ { y } <-> A. x ( ph -> x = y ) )
7		vsnex	|- { y } e. _V
8	7	ssex	|- ( { x | ph } C_ { y } -> { x | ph } e. _V )
9	6 8	sylbir	|- ( A. x ( ph -> x = y ) -> { x | ph } e. _V )
10	9	exlimiv	|- ( E. y A. x ( ph -> x = y ) -> { x | ph } e. _V )
11	1 10	sylbi	|- ( E* x ph -> { x | ph } e. _V )