Theorem nexntru

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

	Ref	Expression
Assertion	nexntru	⊢ ¬ ∃ 𝑥 ¬ ⊤

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2	1	notnoti	⊢ ¬ ¬ ⊤
3	2	nex	⊢ ¬ ∃ 𝑥 ¬ ⊤