Theorem rge0ssre 13516

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3976   class class class wbr 5166  (class class class)co 7448  ℝcr 11183  0cc0 11184  +∞cpnf 11321   ≤ cle 11325  [,)cico 13409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-ico 13413

This theorem is referenced by:  fsumge0  15843  fprodge0  16041  abvf  20838  rege0subm  21464  rge0srg  21479  icopnfhmeo  24993  iccpnfcnv  24994  cphsqrtcl  25237  ovollb2lem  25542  ovollb2  25543  ovolunlem1a  25550  ovolunlem1  25551  ovoliunlem1  25556  ovolicc1  25570  ovolicc2lem4  25574  ovolre  25579  ioombl1lem2  25613  ioombl1lem4  25615  uniioombllem1  25635  uniioombllem2  25637  uniioombllem3  25639  uniioombllem6  25642  0plef  25726  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  itg2mulclem  25801  itg2mulc  25802  itg2monolem1  25805  itg2mono  25808  itg2i1fseq  25810  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  cxpcn3  26809  rlimcnp  27026  efrlim  27030  efrlimOLD  27031  jensenlem1  27048  jensenlem2  27049  jensen  27050  amgm  27052  axcontlem10  29006  ex-fpar  30494  xrge0adddir  33004  fsumrp0cl  33007  xrge0slmod  33341  xrge0iifcnv  33879  lmlimxrge0  33894  rge0scvg  33895  lmdvg  33899  esumfsupre  34035  esumpfinvallem  34038  esumpfinval  34039  esumpfinvalf  34040  esumpcvgval  34042  esumcvg  34050  sibfof  34305  sitgclg  34307  sitgaddlemb  34313  hgt750lemf  34630  hgt750leme  34635  tgoldbachgtde  34637  itg2addnclem2  37632  itg2addnclem3  37633  itg2gt0cn  37635  ftc1anclem3  37655  areacirclem2  37669  xralrple2  45269  ge0xrre  45449  fsumge0cl  45494  liminfresre  45700  fouriersw  46152  sge0rnre  46285  fge0iccre  46295  sge0sn  46300  sge0tsms  46301  sge0f1o  46303  sge0repnf  46307  sge0fsum  46308  sge0pr  46315  sge0ltfirp  46321  sge0resplit  46327  sge0le  46328  sge0split  46330  sge0iunmptlemre  46336  sge0isum  46348  sge0ad2en  46352  sge0isummpt2  46353  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0gtfsumgt  46364  sge0uzfsumgt  46365  sge0seq  46367  sge0reuz  46368  sge0reuzb  46369  meassre  46398  meaiuninclem  46401  omessre  46431  omeiunltfirp  46440  carageniuncl  46444  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hspmbllem1  46547