Theorem rge0ssre 12653

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

Syntax hints:   ∈ wcel 2048   ⊆ wss 3825   class class class wbr 4923  (class class class)co 6970  ℝcr 10326  0cc0 10327  +∞cpnf 10463   ≤ cle 10467  [,)cico 12549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-addrcl 10388  ax-rnegex 10398  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-po 5319  df-so 5320  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-er 8081  df-en 8299  df-dom 8300  df-sdom 8301  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-ico 12553

This theorem is referenced by:  fsumge0  15000  fprodge0  15197  abvf  19306  rege0subm  20293  rge0srg  20308  icopnfhmeo  23240  iccpnfcnv  23241  cphsqrtcl  23481  ovollb2lem  23782  ovollb2  23783  ovolunlem1a  23790  ovolunlem1  23791  ovoliunlem1  23796  ovolicc1  23810  ovolicc2lem4  23814  ovolre  23819  ioombl1lem2  23853  ioombl1lem4  23855  uniioombllem1  23875  uniioombllem2  23877  uniioombllem3  23879  uniioombllem6  23882  0plef  23966  mbfi1fseqlem3  24011  mbfi1fseqlem4  24012  mbfi1fseqlem5  24013  itg2mulclem  24040  itg2mulc  24041  itg2monolem1  24044  itg2mono  24047  itg2i1fseq  24049  itg2gt0  24054  itg2cnlem1  24055  itg2cnlem2  24056  cxpcn3  25020  rlimcnp  25235  efrlim  25239  jensenlem1  25256  jensenlem2  25257  jensen  25258  amgm  25260  axcontlem10  26452  xrge0adddir  30389  fsumrp0cl  30392  xrge0slmod  30552  xrge0iifcnv  30777  lmlimxrge0  30792  rge0scvg  30793  lmdvg  30797  esumfsupre  30931  esumpfinvallem  30934  esumpfinval  30935  esumpfinvalf  30936  esumpcvgval  30938  esumcvg  30946  sibfof  31200  sitgclg  31202  sitgaddlemb  31208  hgt750lemf  31533  hgt750leme  31538  tgoldbachgtde  31540  itg2addnclem2  34333  itg2addnclem3  34334  itg2gt0cn  34336  ftc1anclem3  34358  areacirclem2  34372  xralrple2  40997  ge0xrre  41184  fsumge0cl  41231  liminfresre  41437  fouriersw  41893  sge0rnre  42023  fge0iccre  42033  sge0sn  42038  sge0tsms  42039  sge0f1o  42041  sge0repnf  42045  sge0fsum  42046  sge0pr  42053  sge0ltfirp  42059  sge0resplit  42065  sge0le  42066  sge0split  42068  sge0iunmptlemre  42074  sge0isum  42086  sge0ad2en  42090  sge0isummpt2  42091  sge0xaddlem1  42092  sge0xaddlem2  42093  sge0gtfsumgt  42102  sge0uzfsumgt  42103  sge0seq  42105  sge0reuz  42106  sge0reuzb  42107  meassre  42136  meaiuninclem  42139  omessre  42169  omeiunltfirp  42178  carageniuncl  42182  hoidmvlelem1  42254  hoidmvlelem2  42255  hoidmvlelem3  42256  hoidmvlelem4  42257  hoidmvlelem5  42258  hspmbllem1  42285