Theorem rge0ssre 13378

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3905   class class class wbr 5095  (class class class)co 7353  ℝcr 11027  0cc0 11028  +∞cpnf 11165   ≤ cle 11169  [,)cico 13269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-ico 13273

This theorem is referenced by:  fsumge0  15721  fprodge0  15919  abvf  20719  rege0subm  21349  rge0srg  21364  icopnfhmeo  24858  iccpnfcnv  24859  cphsqrtcl  25101  ovollb2lem  25406  ovollb2  25407  ovolunlem1a  25414  ovolunlem1  25415  ovoliunlem1  25420  ovolicc1  25434  ovolicc2lem4  25438  ovolre  25443  ioombl1lem2  25477  ioombl1lem4  25479  uniioombllem1  25499  uniioombllem2  25501  uniioombllem3  25503  uniioombllem6  25506  0plef  25590  mbfi1fseqlem3  25635  mbfi1fseqlem4  25636  mbfi1fseqlem5  25637  itg2mulclem  25664  itg2mulc  25665  itg2monolem1  25668  itg2mono  25671  itg2i1fseq  25673  itg2gt0  25678  itg2cnlem1  25679  itg2cnlem2  25680  cxpcn3  26675  rlimcnp  26892  efrlim  26896  efrlimOLD  26897  jensenlem1  26914  jensenlem2  26915  jensen  26916  amgm  26918  axcontlem10  28937  ex-fpar  30425  xrge0adddir  32991  fsumrp0cl  32994  xrge0slmod  33304  xrge0iifcnv  33919  lmlimxrge0  33934  rge0scvg  33935  lmdvg  33939  esumfsupre  34057  esumpfinvallem  34060  esumpfinval  34061  esumpfinvalf  34062  esumpcvgval  34064  esumcvg  34072  sibfof  34327  sitgclg  34329  sitgaddlemb  34335  hgt750lemf  34640  hgt750leme  34645  tgoldbachgtde  34647  itg2addnclem2  37671  itg2addnclem3  37672  itg2gt0cn  37674  ftc1anclem3  37694  areacirclem2  37708  xralrple2  45354  ge0xrre  45532  fsumge0cl  45574  liminfresre  45780  fouriersw  46232  sge0rnre  46365  fge0iccre  46375  sge0sn  46380  sge0tsms  46381  sge0f1o  46383  sge0repnf  46387  sge0fsum  46388  sge0pr  46395  sge0ltfirp  46401  sge0resplit  46407  sge0le  46408  sge0split  46410  sge0iunmptlemre  46416  sge0isum  46428  sge0ad2en  46432  sge0isummpt2  46433  sge0xaddlem1  46434  sge0xaddlem2  46435  sge0gtfsumgt  46444  sge0uzfsumgt  46445  sge0seq  46447  sge0reuz  46448  sge0reuzb  46449  meassre  46478  meaiuninclem  46481  omessre  46511  omeiunltfirp  46520  carageniuncl  46524  hoidmvlelem1  46596  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvlelem4  46599  hoidmvlelem5  46600  hspmbllem1  46627  rehalfge1  47339