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

Metamath Proof Explorer

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 ⊤$

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