HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The empty set is not a signed real. |
| Ref | Expression |
|---|---|
| 0nsr |
     |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmenr 6770 |
. . 3
       | |
| 2 | 1 | 0nelqs 5561 |
. 2
 |
| 3 | df-nr 6762 |
. . 3
| |
| 4 | 3 | eleq2i 2237 |
. 2
 |
| 5 | 2, 4 | mtbir 367 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 2
wcel 1617
c0 3114
cxp 4149
cqs 5518
cnp 6580
cer 6587
cnr 6588 |
| This theorem is referenced by: dmaddsr 6789 dmmulsr 6790 addasssr 6792 mulasssr 6794 distrsr 6795 ltasr 6804 recexsrlem 6807 supsrlem1 6820 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1621 ax-gen 1622 ax-8 1623 ax-9 1624 ax-10 1625 ax-11 1626 ax-12 1627 ax-13 1628 ax-14 1629 ax-17 1634 ax-4 1637 ax-5o 1639 ax-6o 1642 ax-9o 1792 ax-10o 1810 ax-16 1883 ax-11o 1893 ax-ext 2152 ax-rep 3628 ax-sep 3638 ax-nul 3645 ax-pow 3681 ax-pr 3719 ax-un 3961 ax-inf2 6008 |
| This theorem depends on definitions: df-bi 232 df-or 434 df-an 435 df-3or 1131 df-3an 1132 df-ex 1645 df-sb 1845 df-eu 2070 df-mo 2071 df-clab 2158 df-cleq 2163 df-clel 2166 df-ne 2297 df-ral 2389 df-rex 2390 df-reu 2391 df-rab 2392 df-v 2571 df-sbc 2731 df-csb 2806 df-dif 2862 df-un 2864 df-in 2866 df-ss 2868 df-pss 2870 df-nul 3115 df-if 3213 df-pw 3261 df-sn 3274 df-pr 3275 df-tp 3277 df-op 3278 df-uni 3399 df-int 3433 df-iun 3470 df-br 3540 df-opab 3598 df-tr 3612 df-eprel 3776 df-id 3779 df-po 3784 df-so 3796 df-fr 3814 df-we 3830 df-ord 3846 df-on 3847 df-lim 3848 df-suc 3849 df-om 4118 df-xp 4165 df-rel 4166 df-cnv 4167 df-co 4168 df-dm 4169 df-rn 4170 df-res 4171 df-ima 4172 df-fun 4173 df-fn 4174 df-f 4175 df-fv 4179 df-opr 5022 df-oprab 5023 df-1st 5166 df-2nd 5167 df-rdg 5344 df-1o 5384 df-oadd 5386 df-omul 5387 df-er 5519 df-ec 5521 df-qs 5524 df-ni 6595 df-pli 6596 df-mi 6597 df-plpq 6630 df-enq 6632 df-nq 6633 df-plq 6634 df-plp 6683 df-enr 6761 df-nr 6762 |