Metamath Proof Explorer


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.