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	|- -. E! x T.

Proof

Step	Hyp	Ref	Expression
1		nexntru	|- -. E. x -. T.
2		eunex	|- ( E! x T. -> E. x -. T. )
3	1 2	mto	|- -. E! x T.