Theorem rge0ssre 13454

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

Syntax hints:   ∈ wcel 2141   ⊆ wss 3902   class class class wbr 5097  (class class class)co 7391  ℝcr 11066  0cc0 11067  +∞cpnf 11207   ≤ cle 11211  [,)cico 13345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-addrcl 11128  ax-rnegex 11138  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-oprab 7395  df-mpo 7396  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-ico 13349

This theorem is referenced by:  fsumge0  15814  fprodge0  16014  abvf  20852  rege0subm  21463  rge0srg  21478  icopnfhmeo  24993  iccpnfcnv  24994  cphsqrtcl  25234  ovollb2lem  25538  ovollb2  25539  ovolunlem1a  25546  ovolunlem1  25547  ovoliunlem1  25552  ovolicc1  25566  ovolicc2lem4  25570  ovolre  25575  ioombl1lem2  25609  ioombl1lem4  25611  uniioombllem1  25631  uniioombllem2  25633  uniioombllem3  25635  uniioombllem6  25638  0plef  25722  mbfi1fseqlem3  25767  mbfi1fseqlem4  25768  mbfi1fseqlem5  25769  itg2mulclem  25796  itg2mulc  25797  itg2monolem1  25800  itg2mono  25803  itg2i1fseq  25805  itg2gt0  25810  itg2cnlem1  25811  itg2cnlem2  25812  cxpcn3  26801  rlimcnp  27018  efrlim  27022  jensenlem1  27039  jensenlem2  27040  jensen  27041  amgm  27043  axcontlem10  29131  ex-fpar  30621  xrge0adddir  33157  fsumrp0cl  33160  xrge0slmod  33495  xrge0iifcnv  34191  lmlimxrge0  34206  rge0scvg  34207  lmdvg  34211  esumfsupre  34329  esumpfinvallem  34332  esumpfinval  34333  esumpfinvalf  34334  esumpcvgval  34336  esumcvg  34344  sibfof  34598  sitgclg  34600  sitgaddlemb  34606  hgt750lemf  34908  hgt750leme  34913  tgoldbachgtde  34915  itg2addnclem2  38132  itg2addnclem3  38133  itg2gt0cn  38135  ftc1anclem3  38155  areacirclem2  38169  xralrple2  45891  ge0xrre  46068  fsumge0cl  46110  liminfresre  46314  fouriersw  46766  sge0rnre  46899  fge0iccre  46909  sge0sn  46914  sge0tsms  46915  sge0f1o  46917  sge0repnf  46921  sge0fsum  46922  sge0pr  46929  sge0ltfirp  46935  sge0resplit  46941  sge0le  46942  sge0split  46944  sge0iunmptlemre  46950  sge0isum  46962  sge0ad2en  46966  sge0isummpt2  46967  sge0xaddlem1  46968  sge0xaddlem2  46969  sge0gtfsumgt  46978  sge0uzfsumgt  46979  sge0seq  46981  sge0reuz  46982  sge0reuzb  46983  meassre  47012  meaiuninclem  47015  omessre  47045  omeiunltfirp  47054  carageniuncl  47058  hoidmvlelem1  47130  hoidmvlelem2  47131  hoidmvlelem3  47132  hoidmvlelem4  47133  hoidmvlelem5  47134  hspmbllem1  47161  rehalfge1  47894