Theorem dfmo2
Rederive [df-mo] from the old definition moeu. (Contributed by Wolf
Lammen, 27-May-2019.) (Proof modification is discouraged.) Use dfmo
instead. (New usage is discouraged.)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
Proof
l0
moeu
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \)
eu6
l2
imbi2i _
\( \vdash \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \)
dfmoeu
\( \vdash \exists x \, \varphi \rightarrow \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (\varphi \rightarrow x = y) \)
3bitri l0 l2 _