Theorem absneu

Description: Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006)

	Ref	Expression
Assertion	absneu	|- ( ( A e. V /\ { x | ph } = { A } ) -> E! x ph )

Proof

Step	Hyp	Ref	Expression
1		sneq	|- ( y = A -> { y } = { A } )
2	1	eqeq2d	|- ( y = A -> ( { x | ph } = { y } <-> { x | ph } = { A } ) )
3	2	spcegv	|- ( A e. V -> ( { x | ph } = { A } -> E. y { x | ph } = { y } ) )
4	3	imp	|- ( ( A e. V /\ { x | ph } = { A } ) -> E. y { x | ph } = { y } )
5		euabsn2	|- ( E! x ph <-> E. y { x | ph } = { y } )
6	4 5	sylibr	|- ( ( A e. V /\ { x | ph } = { A } ) -> E! x ph )