Theorem rge0ssre 13409

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3889   class class class wbr 5085  (class class class)co 7367  ℝcr 11037  0cc0 11038  +∞cpnf 11176   ≤ cle 11180  [,)cico 13300

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-ico 13304

This theorem is referenced by:  fsumge0  15758  fprodge0  15958  abvf  20792  rege0subm  21403  rge0srg  21418  icopnfhmeo  24910  iccpnfcnv  24911  cphsqrtcl  25151  ovollb2lem  25455  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovolicc1  25483  ovolicc2lem4  25487  ovolre  25492  ioombl1lem2  25526  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem3  25552  uniioombllem6  25555  0plef  25639  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  itg2mulclem  25713  itg2mulc  25714  itg2monolem1  25717  itg2mono  25720  itg2i1fseq  25722  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  cxpcn3  26712  rlimcnp  26929  efrlim  26933  jensenlem1  26950  jensenlem2  26951  jensen  26952  amgm  26954  axcontlem10  29042  ex-fpar  30532  xrge0adddir  33078  fsumrp0cl  33081  xrge0slmod  33408  xrge0iifcnv  34077  lmlimxrge0  34092  rge0scvg  34093  lmdvg  34097  esumfsupre  34215  esumpfinvallem  34218  esumpfinval  34219  esumpfinvalf  34220  esumpcvgval  34222  esumcvg  34230  sibfof  34484  sitgclg  34486  sitgaddlemb  34492  hgt750lemf  34797  hgt750leme  34802  tgoldbachgtde  34804  itg2addnclem2  37993  itg2addnclem3  37994  itg2gt0cn  37996  ftc1anclem3  38016  areacirclem2  38030  xralrple2  45784  ge0xrre  45961  fsumge0cl  46003  liminfresre  46207  fouriersw  46659  sge0rnre  46792  fge0iccre  46802  sge0sn  46807  sge0tsms  46808  sge0f1o  46810  sge0repnf  46814  sge0fsum  46815  sge0pr  46822  sge0ltfirp  46828  sge0resplit  46834  sge0le  46835  sge0split  46837  sge0iunmptlemre  46843  sge0isum  46855  sge0ad2en  46859  sge0isummpt2  46860  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0gtfsumgt  46871  sge0uzfsumgt  46872  sge0seq  46874  sge0reuz  46875  sge0reuzb  46876  meassre  46905  meaiuninclem  46908  omessre  46938  omeiunltfirp  46947  carageniuncl  46951  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hspmbllem1  47054  rehalfge1  47787