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

Proof

Step Hyp Ref Expression
1 extru 
 |-  E. x T.
2 neutru 
 |-  -. E! x T.
3 jcn 
 |-  ( E. x T. -> ( -. E! x T. -> -. ( E. x T. -> E! x T. ) ) )
4 1 2 3 mp2 
 |-  -. ( E. x T. -> E! x T. )
5 moeu 
 |-  ( E* x T. <-> ( E. x T. -> E! x T. ) )
6 4 5 mtbir 
 |-  -. E* x T.