Theorem rabsneu

Description: Restricted existential uniqueness determined by a singleton. (Contributed by NM, 29-May-2006) (Revised by Mario Carneiro, 23-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
2	1	eqeq1i	|- ( { x e. B | ph } = { A } <-> { x | ( x e. B /\ ph ) } = { A } )
3		absneu	|- ( ( A e. V /\ { x | ( x e. B /\ ph ) } = { A } ) -> E! x ( x e. B /\ ph ) )
4	2 3	sylan2b	|- ( ( A e. V /\ { x e. B | ph } = { A } ) -> E! x ( x e. B /\ ph ) )
5		df-reu	|- ( E! x e. B ph <-> E! x ( x e. B /\ ph ) )
6	4 5	sylibr	|- ( ( A e. V /\ { x e. B | ph } = { A } ) -> E! x e. B ph )