Theorem exists1

Two ways to express "exactly one thing exists". The left-hand side requires only one variable to express this. Both sides are false in set theory, see Theorem [dtru]. (Contributed by NM, 5-Apr-2004.) (Proof shortened by BJ, 7-Oct-2022.)

Conclusion
\( \vdash \exists{!} x \, x = x \leftrightarrow \forall x \, x = y \)
Proof
equid
bitru _
l2
eubii _
\( \vdash \exists{!} x \, x = x \leftrightarrow \exists{!} x \, \top \)
euae
\( \vdash \exists{!} x \, \top \leftrightarrow \forall x \, x = y \)
bitri l2 _