Theorem rge0ssre 13479

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

Syntax hints:   ∈ wcel 2149   ⊆ wss 3913   class class class wbr 5110  (class class class)co 7408  ℝcr 11095  0cc0 11096  +∞cpnf 11236   ≤ cle 11240  [,)cico 13370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153  ax-1cn 11154  ax-addrcl 11157  ax-rnegex 11167  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-ico 13374

This theorem is referenced by:  fsumge0  15843  fprodge0  16043  abvf  20892  rege0subm  21538  rge0srg  21553  icopnfhmeo  25067  iccpnfcnv  25068  cphsqrtcl  25308  ovollb2lem  25612  ovollb2  25613  ovolunlem1a  25620  ovolunlem1  25621  ovoliunlem1  25626  ovolicc1  25640  ovolicc2lem4  25644  ovolre  25649  ioombl1lem2  25683  ioombl1lem4  25685  uniioombllem1  25705  uniioombllem2  25707  uniioombllem3  25709  uniioombllem6  25712  0plef  25796  mbfi1fseqlem3  25841  mbfi1fseqlem4  25842  mbfi1fseqlem5  25843  itg2mulclem  25870  itg2mulc  25871  itg2monolem1  25874  itg2mono  25877  itg2i1fseq  25879  itg2gt0  25884  itg2cnlem1  25885  itg2cnlem2  25886  cxpcn3  26875  rlimcnp  27092  efrlim  27096  jensenlem1  27113  jensenlem2  27114  jensen  27115  amgm  27117  axcontlem10  29260  ex-fpar  30750  xrge0adddir  33275  fsumrp0cl  33278  xrge0slmod  33607  xrge0iifcnv  34264  lmlimxrge0  34279  rge0scvg  34280  lmdvg  34284  esumfsupre  34402  esumpfinvallem  34405  esumpfinval  34406  esumpfinvalf  34407  esumpcvgval  34409  esumcvg  34417  sibfof  34671  sitgclg  34673  sitgaddlemb  34679  hgt750lemf  34981  hgt750leme  34986  tgoldbachgtde  34988  itg2addnclem2  38206  itg2addnclem3  38207  itg2gt0cn  38209  ftc1anclem3  38229  areacirclem2  38243  xralrple2  45955  ge0xrre  46132  fsumge0cl  46174  liminfresre  46378  fouriersw  46830  sge0rnre  46963  fge0iccre  46973  sge0sn  46978  sge0tsms  46979  sge0f1o  46981  sge0repnf  46985  sge0fsum  46986  sge0pr  46993  sge0ltfirp  46999  sge0resplit  47005  sge0le  47006  sge0split  47008  sge0iunmptlemre  47014  sge0isum  47026  sge0ad2en  47030  sge0isummpt2  47031  sge0xaddlem1  47032  sge0xaddlem2  47033  sge0gtfsumgt  47042  sge0uzfsumgt  47043  sge0seq  47045  sge0reuz  47046  sge0reuzb  47047  meassre  47076  meaiuninclem  47079  omessre  47109  omeiunltfirp  47118  carageniuncl  47122  hoidmvlelem1  47194  hoidmvlelem2  47195  hoidmvlelem3  47196  hoidmvlelem4  47197  hoidmvlelem5  47198  hspmbllem1  47225  rehalfge1  47958