Theorem exmoeub

Existence implies that uniqueness is equivalent to unique existence. (Contributed by NM, 5-Apr-2004.)

Conclusion

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

Proof

df-eu

baibr _