Theorem rge0ssre 13359

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3903   class class class wbr 5092  (class class class)co 7349  ℝcr 11008  0cc0 11009  +∞cpnf 11146   ≤ cle 11150  [,)cico 13250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-addrcl 11070  ax-rnegex 11080  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-ico 13254

This theorem is referenced by:  fsumge0  15702  fprodge0  15900  abvf  20700  rege0subm  21330  rge0srg  21345  icopnfhmeo  24839  iccpnfcnv  24840  cphsqrtcl  25082  ovollb2lem  25387  ovollb2  25388  ovolunlem1a  25395  ovolunlem1  25396  ovoliunlem1  25401  ovolicc1  25415  ovolicc2lem4  25419  ovolre  25424  ioombl1lem2  25458  ioombl1lem4  25460  uniioombllem1  25480  uniioombllem2  25482  uniioombllem3  25484  uniioombllem6  25487  0plef  25571  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  itg2mulclem  25645  itg2mulc  25646  itg2monolem1  25649  itg2mono  25652  itg2i1fseq  25654  itg2gt0  25659  itg2cnlem1  25660  itg2cnlem2  25661  cxpcn3  26656  rlimcnp  26873  efrlim  26877  efrlimOLD  26878  jensenlem1  26895  jensenlem2  26896  jensen  26897  amgm  26899  axcontlem10  28918  ex-fpar  30406  xrge0adddir  32972  fsumrp0cl  32975  xrge0slmod  33285  xrge0iifcnv  33900  lmlimxrge0  33915  rge0scvg  33916  lmdvg  33920  esumfsupre  34038  esumpfinvallem  34041  esumpfinval  34042  esumpfinvalf  34043  esumpcvgval  34045  esumcvg  34053  sibfof  34308  sitgclg  34310  sitgaddlemb  34316  hgt750lemf  34621  hgt750leme  34626  tgoldbachgtde  34628  itg2addnclem2  37652  itg2addnclem3  37653  itg2gt0cn  37655  ftc1anclem3  37675  areacirclem2  37689  xralrple2  45334  ge0xrre  45512  fsumge0cl  45554  liminfresre  45760  fouriersw  46212  sge0rnre  46345  fge0iccre  46355  sge0sn  46360  sge0tsms  46361  sge0f1o  46363  sge0repnf  46367  sge0fsum  46368  sge0pr  46375  sge0ltfirp  46381  sge0resplit  46387  sge0le  46388  sge0split  46390  sge0iunmptlemre  46396  sge0isum  46408  sge0ad2en  46412  sge0isummpt2  46413  sge0xaddlem1  46414  sge0xaddlem2  46415  sge0gtfsumgt  46424  sge0uzfsumgt  46425  sge0seq  46427  sge0reuz  46428  sge0reuzb  46429  meassre  46458  meaiuninclem  46461  omessre  46491  omeiunltfirp  46500  carageniuncl  46504  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  hoidmvlelem5  46580  hspmbllem1  46607  rehalfge1  47319