Theorem dfeumo
An elementary proof showing the reverse direction of dfmoeu. Here
the characterizing expression of existential uniqueness ( eu6) is
derived from that of uniqueness ( [df-mo] ). (Contributed by Wolf
Lammen, 3-Oct-2023.)
Conclusion
\( \vdash \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \rightarrow x = y) \leftrightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
Proof
l0
ax6ev
\( \vdash \exists x \, x = y \)
biimpr
aleximi _
\( \vdash \forall x \, (\varphi \leftrightarrow x = y) \rightarrow \exists x \, x = y \rightarrow \exists x \, \varphi \)
mpi l0 _
exlimiv _
l5
pm4.71ri _
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists x \, \varphi \wedge \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
l6
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)) \)
dfmoeu
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) \)
3bitrri l5 l6 _