Theorem reusn

Description: A way to express restricted existential uniqueness of a wff: its restricted class abstraction is a singleton. (Contributed by NM, 30-May-2006) (Proof shortened by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	reusn	|- ( E! x e. A ph <-> E. y { x e. A | ph } = { y } )

Proof

Step	Hyp	Ref	Expression
1		euabsn2	|- ( E! x ( x e. A /\ ph ) <-> E. y { x | ( x e. A /\ ph ) } = { y } )
2		df-reu	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
4	3	eqeq1i	|- ( { x e. A | ph } = { y } <-> { x | ( x e. A /\ ph ) } = { y } )
5	4	exbii	|- ( E. y { x e. A | ph } = { y } <-> E. y { x | ( x e. A /\ ph ) } = { y } )
6	1 2 5	3bitr4i	|- ( E! x e. A ph <-> E. y { x e. A | ph } = { y } )