Theorem eu3v

An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) Replace a nonfreeness hypothesis with a disjoint variable condition on \( \varphi \), \( y \) to reduce axiom usage. (Revised by Wolf Lammen, 29-May-2019.)

Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
Proof
l0
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
dfmo
anbi2i _
\( \vdash \exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
bitri l0 _