Theorem rge0ssre 13438

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

Syntax hints:   ∈ wcel 2105   ⊆ wss 3948   class class class wbr 5148  (class class class)co 7412  ℝcr 11113  0cc0 11114  +∞cpnf 11250   ≤ cle 11254  [,)cico 13331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-addrcl 11175  ax-rnegex 11185  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-ico 13335

This theorem is referenced by:  fsumge0  15746  fprodge0  15942  abvf  20575  rege0subm  21202  rge0srg  21217  icopnfhmeo  24689  iccpnfcnv  24690  cphsqrtcl  24933  ovollb2lem  25238  ovollb2  25239  ovolunlem1a  25246  ovolunlem1  25247  ovoliunlem1  25252  ovolicc1  25266  ovolicc2lem4  25270  ovolre  25275  ioombl1lem2  25309  ioombl1lem4  25311  uniioombllem1  25331  uniioombllem2  25333  uniioombllem3  25335  uniioombllem6  25338  0plef  25422  mbfi1fseqlem3  25468  mbfi1fseqlem4  25469  mbfi1fseqlem5  25470  itg2mulclem  25497  itg2mulc  25498  itg2monolem1  25501  itg2mono  25504  itg2i1fseq  25506  itg2gt0  25511  itg2cnlem1  25512  itg2cnlem2  25513  cxpcn3  26493  rlimcnp  26707  efrlim  26711  jensenlem1  26728  jensenlem2  26729  jensen  26730  amgm  26732  axcontlem10  28499  ex-fpar  29983  xrge0adddir  32461  fsumrp0cl  32464  xrge0slmod  32734  xrge0iifcnv  33212  lmlimxrge0  33227  rge0scvg  33228  lmdvg  33232  esumfsupre  33368  esumpfinvallem  33371  esumpfinval  33372  esumpfinvalf  33373  esumpcvgval  33375  esumcvg  33383  sibfof  33638  sitgclg  33640  sitgaddlemb  33646  hgt750lemf  33964  hgt750leme  33969  tgoldbachgtde  33971  itg2addnclem2  36844  itg2addnclem3  36845  itg2gt0cn  36847  ftc1anclem3  36867  areacirclem2  36881  xralrple2  44363  ge0xrre  44543  fsumge0cl  44588  liminfresre  44794  fouriersw  45246  sge0rnre  45379  fge0iccre  45389  sge0sn  45394  sge0tsms  45395  sge0f1o  45397  sge0repnf  45401  sge0fsum  45402  sge0pr  45409  sge0ltfirp  45415  sge0resplit  45421  sge0le  45422  sge0split  45424  sge0iunmptlemre  45430  sge0isum  45442  sge0ad2en  45446  sge0isummpt2  45447  sge0xaddlem1  45448  sge0xaddlem2  45449  sge0gtfsumgt  45458  sge0uzfsumgt  45459  sge0seq  45461  sge0reuz  45462  sge0reuzb  45463  meassre  45492  meaiuninclem  45495  omessre  45525  omeiunltfirp  45534  carageniuncl  45538  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  hoidmvlelem5  45614  hspmbllem1  45641