This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exmo

Description: 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)

		Ref	Expression
	Assertion	exmo	$⊢ (\exists x φ \lor \exists^{*} x φ)$

Proof

Step	Hyp	Ref	Expression
1		nexmo	$⊢ \neg \exists x φ \to \exists^{*} x φ$
2	1	orri	$⊢ (\exists x φ \lor \exists^{*} x φ)$