Theorem nmotru

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

	Ref	Expression
Assertion	nmotru	$$⊢\neg {\exists }^{*}x\top$$

Proof

Step	Hyp	Ref	Expression
1		extru	$$⊢\exists x\top$$
2		neutru	$$⊢\neg \exists !x\top$$
3		jcn	$$⊢\exists x\top \to \left(\neg \exists !x\top \to \neg \left(\exists x\top \to \exists !x\top \right)\right)$$
4	1 2 3	mp2	$$⊢\neg \left(\exists x\top \to \exists !x\top \right)$$
5		moeu	$$⊢{\exists }^{*}x\top \leftrightarrow \left(\exists x\top \to \exists !x\top \right)$$
6	4 5	mtbir	$$⊢\neg {\exists }^{*}x\top$$