Theorem euae
Two ways to express "exactly one thing exists". To paraphrase the
statement and explain the label: there Exists a Unique thing if and only
if for All \( x \), \( x \) Equals some given (and disjoint) \( y \). Both
sides are false in set theory, see Theorems [neutru] and [dtru].
(Contributed by NM, 5-Apr-2004.) State the theorem using truth constant
\( \top \). (Revised by BJ, 7-Oct-2022.) Reduce axiom dependencies.
(Revised by Wolf Lammen, 2-Mar-2023.)
Conclusion
\( \vdash \exists{!} x \, \top \leftrightarrow \forall x \, x = y \)
Proof
extru
l1
biantrur _
\( \vdash \exists y \, \forall x \, (\top \rightarrow x = y) \leftrightarrow \exists x \, \top \wedge \exists y \, \forall x \, (\top \rightarrow x = y) \)
hbaev
l3
19.8w _
l4
hbnaev
\( \vdash \neg \forall x \, x = y \rightarrow \forall y \, \neg \forall x \, x = y \)
alnex
\( \vdash \forall y \, \neg \forall x \, x = y \leftrightarrow \neg \exists y \, \forall x \, x = y \)
sylib l4 _
con4i _
l8
impbii l3 _
\( \vdash \forall x \, x = y \leftrightarrow \exists y \, \forall x \, x = y \)
trut
albii _
exbii _
\( \vdash \exists y \, \forall x \, x = y \leftrightarrow \exists y \, \forall x \, (\top \rightarrow x = y) \)
l12
bitri l8 _
\( \vdash \forall x \, x = y \leftrightarrow \exists y \, \forall x \, (\top \rightarrow x = y) \)
eu3v
\( \vdash \exists{!} x \, \top \leftrightarrow \exists x \, \top \wedge \exists y \, \forall x \, (\top \rightarrow x = y) \)
3bitr4ri l1 l12 _