Theorem rge0ssre 13400

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 13398	. . 3 ⊢ (𝑥 ∈ (0[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
2	1	simplbi 496	. 2 ⊢ (𝑥 ∈ (0[,)+∞) → 𝑥 ∈ ℝ)
3	2	ssriv 3926	1 ⊢ (0[,)+∞) ⊆ ℝ

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890   class class class wbr 5086  (class class class)co 7360  ℝcr 11028  0cc0 11029  +∞cpnf 11167   ≤ cle 11171  [,)cico 13291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-ico 13295

This theorem is referenced by:  fsumge0  15749  fprodge0  15949  abvf  20783  rege0subm  21413  rge0srg  21428  icopnfhmeo  24920  iccpnfcnv  24921  cphsqrtcl  25161  ovollb2lem  25465  ovollb2  25466  ovolunlem1a  25473  ovolunlem1  25474  ovoliunlem1  25479  ovolicc1  25493  ovolicc2lem4  25497  ovolre  25502  ioombl1lem2  25536  ioombl1lem4  25538  uniioombllem1  25558  uniioombllem2  25560  uniioombllem3  25562  uniioombllem6  25565  0plef  25649  mbfi1fseqlem3  25694  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  itg2mulclem  25723  itg2mulc  25724  itg2monolem1  25727  itg2mono  25730  itg2i1fseq  25732  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  cxpcn3  26725  rlimcnp  26942  efrlim  26946  efrlimOLD  26947  jensenlem1  26964  jensenlem2  26965  jensen  26966  amgm  26968  axcontlem10  29056  ex-fpar  30547  xrge0adddir  33093  fsumrp0cl  33096  xrge0slmod  33423  xrge0iifcnv  34093  lmlimxrge0  34108  rge0scvg  34109  lmdvg  34113  esumfsupre  34231  esumpfinvallem  34234  esumpfinval  34235  esumpfinvalf  34236  esumpcvgval  34238  esumcvg  34246  sibfof  34500  sitgclg  34502  sitgaddlemb  34508  hgt750lemf  34813  hgt750leme  34818  tgoldbachgtde  34820  itg2addnclem2  38007  itg2addnclem3  38008  itg2gt0cn  38010  ftc1anclem3  38030  areacirclem2  38044  xralrple2  45802  ge0xrre  45979  fsumge0cl  46021  liminfresre  46225  fouriersw  46677  sge0rnre  46810  fge0iccre  46820  sge0sn  46825  sge0tsms  46826  sge0f1o  46828  sge0repnf  46832  sge0fsum  46833  sge0pr  46840  sge0ltfirp  46846  sge0resplit  46852  sge0le  46853  sge0split  46855  sge0iunmptlemre  46861  sge0isum  46873  sge0ad2en  46877  sge0isummpt2  46878  sge0xaddlem1  46879  sge0xaddlem2  46880  sge0gtfsumgt  46889  sge0uzfsumgt  46890  sge0seq  46892  sge0reuz  46893  sge0reuzb  46894  meassre  46923  meaiuninclem  46926  omessre  46956  omeiunltfirp  46965  carageniuncl  46969  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hspmbllem1  47072  rehalfge1  47799