Theorem reex 10628

Description: The real numbers form a set. See also reexALT 12384. (Contributed by Mario Carneiro, 17-Nov-2014.)

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10618	. 2 ⊢ ℂ ∈ V
2		ax-resscn 10594	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5226	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494  ℂcc 10535  ℝcr 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  reelprrecn  10629  negfi  11589  xrex  12387  limsuple  14835  limsuplt  14836  limsupbnd1  14839  rlim  14852  rlimf  14858  rlimss  14859  ello12  14873  lo1f  14875  lo1dm  14876  elo12  14884  o1f  14886  o1dm  14887  o1of2  14969  o1rlimmul  14975  o1add2  14980  o1mul2  14981  o1sub2  14982  o1dif  14986  caucvgrlem  15029  fsumo1  15167  rpnnen  15580  cpnnen  15582  ruclem13  15595  ruc  15596  aleph1re  15598  aleph1irr  15599  cnfldds  20555  replusg  20754  remulr  20755  rele2  20758  reds  20760  refldcj  20764  ismet  22933  tngngp2  23261  tngngpd  23262  tngngp  23263  tngngp3  23265  nrmtngnrm  23267  tngnrg  23283  rerest  23412  xrtgioo  23414  xrrest  23415  xrsmopn  23420  opnreen  23439  rectbntr0  23440  xrge0tsms  23442  bcthlem1  23927  bcthlem5  23931  reust  23984  rrxip  23993  rrx0el  24001  ehl0base  24019  ehl1eudis  24023  ehl2eudis  24025  pmltpclem2  24050  ovolficcss  24070  ovolval  24074  elovolmlem  24075  ovolctb2  24093  ismbl  24127  mblsplit  24133  voliunlem3  24153  dyadmbl  24201  vitalilem2  24210  vitalilem3  24211  vitalilem4  24212  vitalilem5  24213  vitali  24214  mbff  24226  ismbf  24229  ismbfcn  24230  mbfconst  24234  cncombf  24259  cnmbf  24260  0plef  24273  i1fd  24282  itg1ge0  24287  i1faddlem  24294  i1fmullem  24295  i1fadd  24296  i1fmul  24297  itg1addlem4  24300  i1fmulclem  24303  i1fmulc  24304  itg1mulc  24305  i1fsub  24309  itg1sub  24310  itg1lea  24313  itg1le  24314  mbfi1fseqlem2  24317  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1flimlem  24323  mbfmullem2  24325  itg2val  24329  xrge0f  24332  itg2ge0  24336  itg2itg1  24337  itg20  24338  itg2le  24340  itg2const  24341  itg2const2  24342  itg2seq  24343  itg2uba  24344  itg2lea  24345  itg2mulclem  24347  itg2mulc  24348  itg2splitlem  24349  itg2split  24350  itg2monolem1  24351  itg2mono  24354  itg2i1fseqle  24355  itg2i1fseq  24356  itg2addlem  24359  itg2gt0  24361  itg2cnlem1  24362  itg2cnlem2  24363  iblss  24405  i1fibl  24408  itgitg1  24409  itgle  24410  ibladdlem  24420  itgaddlem1  24423  iblabslem  24428  iblabs  24429  iblabsr  24430  iblmulc2  24431  itgmulc2lem1  24432  bddmulibl  24439  dvnfre  24549  c1liplem1  24593  c1lip2  24595  lhop2  24612  dvcnvrelem2  24615  taylthlem2  24962  dmarea  25535  vmadivsum  26058  rpvmasumlem  26063  mudivsum  26106  selberglem1  26121  selberglem2  26122  selberg2lem  26126  selberg2  26127  pntrsumo1  26141  selbergr  26144  iscgrgd  26299  elee  26680  xrge0tsmsd  30692  nn0omnd  30914  xrge0slmod  30917  raddcn  31172  rrhcn  31238  qqtopn  31252  dmvlsiga  31388  ddeval1  31493  ddeval0  31494  ddemeas  31495  mbfmcnt  31526  sxbrsigalem0  31529  sxbrsigalem3  31530  sxbrsigalem2  31544  isrrvv  31701  dstfrvclim1  31735  signsplypnf  31820  erdsze2lem1  32450  erdsze2lem2  32451  snmlval  32578  knoppcnlem5  33836  knoppcnlem6  33837  knoppcnlem7  33838  knoppcnlem8  33839  cnndvlem2  33877  icoreresf  34636  icoreval  34637  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimir  34940  broucube  34941  mblfinlem3  34946  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  itg2gt0cn  34962  ibladdnclem  34963  itgaddnclem1  34965  iblabsnclem  34970  iblabsnc  34971  iblmulc2nc  34972  itgmulc2nclem1  34973  bddiblnc  34977  ftc1anclem3  34984  ftc1anclem4  34985  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  filbcmb  35030  rrncmslem  35125  repwsmet  35127  rrnequiv  35128  ismrer1  35131  pell1qrval  39492  pell14qrval  39494  pell1234qrval  39496  k0004ss1  40550  addrval  40847  subrval  40848  mulvval  40849  climreeq  41943  limsupre  41971  limcresiooub  41972  limcresioolb  41973  limsuppnfdlem  42031  limsuppnflem  42040  limsupmnflem  42050  limsupre2lem  42054  xlimclim  42154  icccncfext  42219  cncfiooicclem1  42225  itgsubsticclem  42309  ovolsplit  42322  dirkerval  42425  dirkercncflem4  42440  fourierdlem14  42455  fourierdlem15  42456  fourierdlem32  42473  fourierdlem33  42474  fourierdlem54  42494  fourierdlem62  42502  fourierdlem70  42510  fourierdlem81  42521  fourierdlem92  42532  fourierdlem102  42542  fourierdlem111  42551  fourierdlem114  42554  etransclem2  42570  rrxtopn0  42627  qndenserrnbllem  42628  qndenserrnbl  42629  qndenserrn  42633  rrnprjdstle  42635  ioorrnopnlem  42638  dmvolsal  42678  hoicvr  42879  hoissrrn  42880  hoiprodcl2  42886  hoicvrrex  42887  ovn0lem  42896  ovn02  42899  hsphoif  42907  hoidmvval  42908  hoissrrn2  42909  hsphoival  42910  hoidmvlelem3  42928  hoidmvle  42931  ovnhoilem1  42932  ovnhoilem2  42933  ovnhoi  42934  hspval  42940  ovnlecvr2  42941  ovncvr2  42942  hoidifhspval2  42946  hoiqssbl  42956  hspmbllem2  42958  hspmbl  42960  hoimbl  42962  opnvonmbllem2  42964  ovolval2lem  42974  ovolval2  42975  ovolval3  42978  ovolval4lem2  42981  ovolval5lem2  42984  ovnovollem1  42987  ovnovollem2  42988  ovnovollem3  42989  vonvolmbllem  42991  vonvolmbl  42992  vitali2  43025  issmflem  43053  incsmf  43068  decsmf  43092  nsssmfmbflem  43103  smfresal  43112  smfmullem4  43118  smf2id  43125  refdivpm  44653  elbigo2  44661  elbigof  44663  elbigodm  44664  elbigoimp  44665  elbigolo1  44666  prelrrx2  44749  rrx2xpref1o  44754  rrx2xpreen  44755  rrx2linesl  44779  line2  44788  line2x  44790  line2y  44791  amgmlemALT  44953