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 5147 |
. . 3
       | |
| 2 | 1 | 0nelqs 4282 |
. 2
 |
| 3 | df-nr 5139 |
. . 3
| |
| 4 | 3 | eleq2i 1530 |
. 2
 |
| 5 | 2, 4 | mtbir 192 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 2
wcel 955
c0 2270
cxp 3158
cqs 4244
cnp 4957
cer 4964
cnr 4965 |
| This theorem is referenced by: dmaddsr 5166 dmmulsr 5167 addasssr 5169 mulasssr 5171 distrsr 5172 ltasr 5181 recexsrlem 5184 supsrlem1 5197 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-ni 4972 df-pli 4973 df-mi 4974 df-plpq 5007 df-enq 5009 df-nq 5010 df-plq 5011 df-plp 5060 df-enr 5138 df-nr 5139 |