Theorem neutru

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

	Ref	Expression
Assertion	neutru	⊢ ¬ ∃! 𝑥 ⊤

Proof

Step	Hyp	Ref	Expression
1		nexntru	⊢ ¬ ∃ 𝑥 ¬ ⊤
2		eunex	⊢ ( ∃! 𝑥 ⊤ → ∃ 𝑥 ¬ ⊤ )
3	1 2	mto	⊢ ¬ ∃! 𝑥 ⊤