Theorem moeuex

Uniqueness implies that existence is equivalent to unique existence. (Contributed by BJ, 7-Oct-2022.)

Conclusion

\( \vdash \exists^\ast x \, \varphi \rightarrow (\exists x \, \varphi \leftrightarrow \exists{!} x \, \varphi) \)

Proof

df-eu

rbaibr _