Theorem rge0ssre 13484

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

Syntax hints:   ∈ wcel 2143   ⊆ wss 3906   class class class wbr 5110  (class class class)co 7412  ℝcr 11100  0cc0 11101  +∞cpnf 11241   ≤ cle 11245  [,)cico 13375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-addrcl 11162  ax-rnegex 11172  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-ico 13379

This theorem is referenced by:  fsumge0  15849  fprodge0  16049  abvf  20899  rege0subm  21554  rge0srg  21569  icopnfhmeo  25083  iccpnfcnv  25084  cphsqrtcl  25324  ovollb2lem  25628  ovollb2  25629  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovolicc1  25656  ovolicc2lem4  25660  ovolre  25665  ioombl1lem2  25699  ioombl1lem4  25701  uniioombllem1  25721  uniioombllem2  25723  uniioombllem3  25725  uniioombllem6  25728  0plef  25812  mbfi1fseqlem3  25857  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  itg2mulclem  25886  itg2mulc  25887  itg2monolem1  25890  itg2mono  25893  itg2i1fseq  25895  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  cxpcn3  26894  rlimcnp  27111  efrlim  27115  jensenlem1  27132  jensenlem2  27133  jensen  27134  amgm  27136  axcontlem10  29304  ex-fpar  30794  xrge0adddir  33319  fsumrp0cl  33322  xrge0slmod  33649  xrge0iifcnv  34304  lmlimxrge0  34319  rge0scvg  34320  lmdvg  34324  esumfsupre  34442  esumpfinvallem  34445  esumpfinval  34446  esumpfinvalf  34447  esumpcvgval  34449  esumcvg  34457  sibfof  34711  sitgclg  34713  sitgaddlemb  34719  hgt750lemf  35021  hgt750leme  35026  tgoldbachgtde  35028  itg2addnclem2  38304  itg2addnclem3  38305  itg2gt0cn  38307  ftc1anclem3  38327  areacirclem2  38341  xralrple2  46053  ge0xrre  46230  fsumge0cl  46272  liminfresre  46476  fouriersw  46928  sge0rnre  47061  fge0iccre  47071  sge0sn  47076  sge0tsms  47077  sge0f1o  47079  sge0repnf  47083  sge0fsum  47084  sge0pr  47091  sge0ltfirp  47097  sge0resplit  47103  sge0le  47104  sge0split  47106  sge0iunmptlemre  47112  sge0isum  47124  sge0ad2en  47128  sge0isummpt2  47129  sge0xaddlem1  47130  sge0xaddlem2  47131  sge0gtfsumgt  47140  sge0uzfsumgt  47141  sge0seq  47143  sge0reuz  47144  sge0reuzb  47145  meassre  47174  meaiuninclem  47177  omessre  47207  omeiunltfirp  47216  carageniuncl  47220  hoidmvlelem1  47292  hoidmvlelem2  47293  hoidmvlelem3  47294  hoidmvlelem4  47295  hoidmvlelem5  47296  hspmbllem1  47323  rehalfge1  48059