Metamath Proof Explorer


Theorem 0nsr

Description: The empty set is not a signed real. (Contributed by NM, 25-Aug-1995) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

Ref Expression
Assertion 0nsr
|- -. (/) e. R.

Proof

Step Hyp Ref Expression
1 eqid
 |-  (/) = (/)
2 enrer
 |-  ~R Er ( P. X. P. )
3 erdm
 |-  ( ~R Er ( P. X. P. ) -> dom ~R = ( P. X. P. ) )
4 2 3 ax-mp
 |-  dom ~R = ( P. X. P. )
5 elqsn0
 |-  ( ( dom ~R = ( P. X. P. ) /\ (/) e. ( ( P. X. P. ) /. ~R ) ) -> (/) =/= (/) )
6 4 5 mpan
 |-  ( (/) e. ( ( P. X. P. ) /. ~R ) -> (/) =/= (/) )
7 df-nr
 |-  R. = ( ( P. X. P. ) /. ~R )
8 6 7 eleq2s
 |-  ( (/) e. R. -> (/) =/= (/) )
9 8 necon2bi
 |-  ( (/) = (/) -> -. (/) e. R. )
10 1 9 ax-mp
 |-  -. (/) e. R.