Theorem exmo

Any proposition holds for some \( x \) or holds for at most one \( x \). (Contributed by NM, 8-Mar-1995.) Shorten proof and avoid [df-eu]. (Revised by BJ, 14-Oct-2022.)

Conclusion
\( \vdash \exists x \, \varphi \vee \exists^\ast x \, \varphi \)
Proof
nexmo
orri _