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	$$⊢\exists !x\phi \leftrightarrow \exists !y\left\{x|\phi \right\}=\left\{y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mosneq	$$⊢{\exists }^{*}y\left\{y\right\}=\left\{x|\phi \right\}$$
2		eqcom	$$⊢\left\{y\right\}=\left\{x|\phi \right\}\leftrightarrow \left\{x|\phi \right\}=\left\{y\right\}$$
3	2	mobii	$$⊢{\exists }^{*}y\left\{y\right\}=\left\{x|\phi \right\}\leftrightarrow {\exists }^{*}y\left\{x|\phi \right\}=\left\{y\right\}$$
4	1 3	mpbi	$$⊢{\exists }^{*}y\left\{x|\phi \right\}=\left\{y\right\}$$
5	4	biantru	$$⊢\exists y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \left(\exists y\left\{x|\phi \right\}=\left\{y\right\}\wedge {\exists }^{*}y\left\{x|\phi \right\}=\left\{y\right\}\right)$$
6		euabsn2	$$⊢\exists !x\phi \leftrightarrow \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
7		df-eu	$$⊢\exists !y\left\{x|\phi \right\}=\left\{y\right\}\leftrightarrow \left(\exists y\left\{x|\phi \right\}=\left\{y\right\}\wedge {\exists }^{*}y\left\{x|\phi \right\}=\left\{y\right\}\right)$$
8	5 6 7	3bitr4i	$$⊢\exists !x\phi \leftrightarrow \exists !y\left\{x|\phi \right\}=\left\{y\right\}$$