Theorem dfmoeu
An elementary proof of moeu in disguise, connecting an expression
characterizing uniqueness ( [df-mo]) to that of existential uniqueness
( eu6 ). No particular order of definition is required, as one can be
derived from the other. This is shown here and in dfeumo.
(Contributed by Wolf Lammen, 27-May-2019.)
Conclusion
\( \vdash \exists x \, \varphi \rightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
Proof
l0
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
pm2.21
alimi _
\( \vdash \forall x \, \neg \varphi \rightarrow \forall x \, (\varphi \rightarrow x = y) \)
sylbir l0 _
l4
19.8ad _
biimp
alimi _
eximi _
l8
ja l4 _
l9
nfia1
l10
id
ax12v
com12 _
embantd l10 _
spsd _
l15
ancld _
\( \vdash \varphi \rightarrow \forall x \, (\varphi \rightarrow x = y) \rightarrow \forall x \, (\varphi \rightarrow x = y) \wedge \forall x \, (x = y \rightarrow \varphi) \)
albiim
\( \vdash \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \forall x \, (\varphi \rightarrow x = y) \wedge \forall x \, (x = y \rightarrow \varphi) \)
imbitrrdi l15 _
exlimi l9 _
eximdv _
com12 _
impbii l8 _