Theorem rge0ssre 13363

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

Syntax hints:   ∈ wcel 2113   ⊆ wss 3898   class class class wbr 5095  (class class class)co 7355  ℝcr 11016  0cc0 11017  +∞cpnf 11154   ≤ cle 11158  [,)cico 13254

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074  ax-1cn 11075  ax-addrcl 11078  ax-rnegex 11088  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-ico 13258

This theorem is referenced by:  fsumge0  15709  fprodge0  15907  abvf  20739  rege0subm  21369  rge0srg  21384  icopnfhmeo  24888  iccpnfcnv  24889  cphsqrtcl  25131  ovollb2lem  25436  ovollb2  25437  ovolunlem1a  25444  ovolunlem1  25445  ovoliunlem1  25450  ovolicc1  25464  ovolicc2lem4  25468  ovolre  25473  ioombl1lem2  25507  ioombl1lem4  25509  uniioombllem1  25529  uniioombllem2  25531  uniioombllem3  25533  uniioombllem6  25536  0plef  25620  mbfi1fseqlem3  25665  mbfi1fseqlem4  25666  mbfi1fseqlem5  25667  itg2mulclem  25694  itg2mulc  25695  itg2monolem1  25698  itg2mono  25701  itg2i1fseq  25703  itg2gt0  25708  itg2cnlem1  25709  itg2cnlem2  25710  cxpcn3  26705  rlimcnp  26922  efrlim  26926  efrlimOLD  26927  jensenlem1  26944  jensenlem2  26945  jensen  26946  amgm  26948  axcontlem10  28972  ex-fpar  30463  xrge0adddir  33028  fsumrp0cl  33031  xrge0slmod  33357  xrge0iifcnv  34018  lmlimxrge0  34033  rge0scvg  34034  lmdvg  34038  esumfsupre  34156  esumpfinvallem  34159  esumpfinval  34160  esumpfinvalf  34161  esumpcvgval  34163  esumcvg  34171  sibfof  34425  sitgclg  34427  sitgaddlemb  34433  hgt750lemf  34738  hgt750leme  34743  tgoldbachgtde  34745  itg2addnclem2  37785  itg2addnclem3  37786  itg2gt0cn  37788  ftc1anclem3  37808  areacirclem2  37822  xralrple2  45515  ge0xrre  45693  fsumge0cl  45735  liminfresre  45939  fouriersw  46391  sge0rnre  46524  fge0iccre  46534  sge0sn  46539  sge0tsms  46540  sge0f1o  46542  sge0repnf  46546  sge0fsum  46547  sge0pr  46554  sge0ltfirp  46560  sge0resplit  46566  sge0le  46567  sge0split  46569  sge0iunmptlemre  46575  sge0isum  46587  sge0ad2en  46591  sge0isummpt2  46592  sge0xaddlem1  46593  sge0xaddlem2  46594  sge0gtfsumgt  46603  sge0uzfsumgt  46604  sge0seq  46606  sge0reuz  46607  sge0reuzb  46608  meassre  46637  meaiuninclem  46640  omessre  46670  omeiunltfirp  46679  carageniuncl  46683  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvlelem4  46758  hoidmvlelem5  46759  hspmbllem1  46786  rehalfge1  47497