Theorem rge0ssre 12494

Description: Nonnegative real numbers are real numbers. (Contributed by Thierry Arnoux, 9-Sep-2018.) (Proof shortened by AV, 8-Sep-2019.)

Assertion

Ref	Expression
rge0ssre	⊢ (0[,)+∞) ⊆ ℝ

Proof of Theorem rge0ssre

Step	Hyp	Ref	Expression
1		elrege0 12492	. . 3 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
2	1	simplbi 487	. 2 ⊢ (𝑥 ∈ (0[,)+∞) → 𝑥 ∈ ℝ)
3	2	ssriv 3796	1 ⊢ (0[,)+∞) ⊆ ℝ

Syntax hints:   ∈ wcel 2155   ⊆ wss 3763   class class class wbr 4837  (class class class)co 6868  ℝcr 10214  0cc0 10215  +∞cpnf 10350   ≤ cle 10354  [,)cico 12389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-i2m1 10283  ax-1ne0 10284  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-po 5226  df-so 5227  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-er 7973  df-en 8187  df-dom 8188  df-sdom 8189  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-ico 12393

This theorem is referenced by:  fsumge0  14743  abvf  19021  rege0subm  20004  rge0srg  20019  icopnfhmeo  22949  iccpnfcnv  22950  cphsqrtcl  23190  ovollb2lem  23463  ovollb2  23464  ovolunlem1a  23471  ovolunlem1  23472  ovoliunlem1  23477  ovolicc1  23491  ovolicc2lem4  23495  ovolre  23500  ioombl1lem2  23534  ioombl1lem4  23536  uniioombllem1  23556  uniioombllem2  23558  uniioombllem3  23560  uniioombllem6  23563  0plef  23647  mbfi1fseqlem3  23692  mbfi1fseqlem4  23693  mbfi1fseqlem5  23694  itg2mulclem  23721  itg2mulc  23722  itg2monolem1  23725  itg2mono  23728  itg2i1fseq  23730  itg2gt0  23735  itg2cnlem1  23736  itg2cnlem2  23737  cxpcn3  24697  rlimcnp  24900  efrlim  24904  jensenlem1  24921  jensenlem2  24922  jensen  24923  amgm  24925  axcontlem10  26061  xrge0adddir  30011  fsumrp0cl  30014  xrge0slmod  30163  xrge0iifcnv  30298  lmlimxrge0  30313  rge0scvg  30314  lmdvg  30318  esumfsupre  30452  esumpfinvallem  30455  esumpfinval  30456  esumpfinvalf  30457  esumpcvgval  30459  esumcvg  30467  sibfof  30721  sitgclg  30723  sitgaddlemb  30729  hgt750lemf  31050  hgt750leme  31055  tgoldbachgtde  31057  itg2addnclem2  33768  itg2addnclem3  33769  itg2gt0cn  33771  ftc1anclem3  33793  areacirclem2  33807  xralrple2  40044  ge0xrre  40232  fsumge0cl  40279  liminfresre  40485  fouriersw  40921  sge0rnre  41054  fge0iccre  41064  sge0sn  41069  sge0tsms  41070  sge0f1o  41072  sge0repnf  41076  sge0fsum  41077  sge0pr  41084  sge0ltfirp  41090  sge0resplit  41096  sge0le  41097  sge0split  41099  sge0iunmptlemre  41105  sge0isum  41117  sge0ad2en  41121  sge0isummpt2  41122  sge0xaddlem1  41123  sge0xaddlem2  41124  sge0gtfsumgt  41133  sge0uzfsumgt  41134  sge0seq  41136  sge0reuz  41137  sge0reuzb  41138  meassre  41167  meaiuninclem  41170  omessre  41200  omeiunltfirp  41209  carageniuncl  41213  hoidmvlelem1  41285  hoidmvlelem2  41286  hoidmvlelem3  41287  hoidmvlelem4  41288  hoidmvlelem5  41289  hspmbllem1  41316