Theorem eu6
Alternate definition of the unique existential quantifier [df-eu] not
using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993.)
This used to be the definition of the unique existential quantifier,
while [df-eu] was then proved as dfeu. (Revised by BJ, 30-Sep-2022.)
(Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of [ax-11].
(Revised by SN, 21-Sep-2023.)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
Proof
dfmoeu
l1
anbi2i _
\( \vdash \exists x \, \varphi \wedge (\exists x \, \varphi \rightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y)) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
l2
abai
\( \vdash \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists x \, \varphi \wedge (\exists x \, \varphi \rightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y)) \)
eu3v
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
l4
3bitr4ri l1 l2 _
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
l5
abai
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \wedge \exists x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \wedge (\exists y \, \forall x \, (\varphi \leftrightarrow x = y) \rightarrow \exists x \, \varphi) \)
l6
ancom
\( \vdash \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \wedge \exists x \, \varphi \)
biimpr
alimi _
l9
eximi _
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \rightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \)
exsbim
\( \vdash \exists y \, \forall x \, (x = y \rightarrow \varphi) \rightarrow \exists x \, \varphi \)
syl l9 _
biantru _
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \wedge (\exists y \, \forall x \, (\varphi \leftrightarrow x = y) \rightarrow \exists x \, \varphi) \)
3bitr4i l5 l6 _
\( \vdash \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
bitri l4 _