Theorem euabsneu

Description: Another way to express existential uniqueness of a wff ph : its associated class abstraction { x | ph } is a singleton. Variant of euabsn2 using existential uniqueness for the singleton element instead of existence only. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	euabsneu	|- ( E! x ph <-> E! y { x | ph } = { y } )

Proof

Step	Hyp	Ref	Expression
1		mosneq	|- E* y { y } = { x | ph }
2		eqcom	|- ( { y } = { x | ph } <-> { x | ph } = { y } )
3	2	mobii	|- ( E* y { y } = { x | ph } <-> E* y { x | ph } = { y } )
4	1 3	mpbi	|- E* y { x | ph } = { y }
5	4	biantru	|- ( E. y { x | ph } = { y } <-> ( E. y { x | ph } = { y } /\ E* y { x | ph } = { y } ) )
6		euabsn2	|- ( E! x ph <-> E. y { x | ph } = { y } )
7		df-eu	|- ( E! y { x | ph } = { y } <-> ( E. y { x | ph } = { y } /\ E* y { x | ph } = { y } ) )
8	5 6 7	3bitr4i	|- ( E! x ph <-> E! y { x | ph } = { y } )