Theorem mofal

Description: There exist at most one set such that F. is true. (Contributed by Anthony Hart, 13-Sep-2011)

	Ref	Expression
Assertion	mofal	$$⊢{\exists }^{*}x\perp$$

Proof

Step	Hyp	Ref	Expression
1		nexfal	$$⊢\neg \exists x\perp$$
2		exmo	$$⊢\left(\exists x\perp \vee {\exists }^{*}x\perp \right)$$
3	1 2	mtpor	$$⊢{\exists }^{*}x\perp$$