Theorem reex 11215

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11205	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11181	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5287	1 ⊢ ℝ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ℂcc 11122  ℝcr 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-cnex 11180  ax-resscn 11181

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916

This theorem is used by:  reelprrecn  11216  negfi  12188  xrex  13037  limsuple  15565  limsuplt  15566  limsupbnd1  15569  rlim  15582  rlimf  15588  rlimss  15589  ello12  15603  lo1f  15605  lo1dm  15606  elo12  15614  o1f  15616  o1dm  15617  o1of2  15700  o1rlimmul  15706  o1add2  15711  o1mul2  15712  o1sub2  15713  o1dif  15717  caucvgrlem  15760  fsumo1  15899  rpnnen  16315  cpnnen  16317  ruclem13  16330  ruc  16331  aleph1re  16333  aleph1irr  16334  cnfldds  21597  replusg  21823  remulr  21824  rele2  21827  reds  21829  refldcj  21833  ismet  24549  tngngp2  24878  tngngpd  24879  tngngp  24880  tngngp3  24882  nrmtngnrm  24884  tngnrg  24900  rerest  25030  xrtgioo  25033  xrrest  25034  xrsmopn  25039  opnreen  25058  rectbntr0  25059  xrge0tsms  25061  bcthlem1  25552  bcthlem5  25556  reust  25609  rrxip  25618  rrx0el  25626  ehl0base  25644  ehl1eudis  25648  ehl2eudis  25650  pmltpclem2  25677  ovolficcss  25697  ovolval  25701  elovolmlem  25702  ovolctb2  25720  ismbl  25754  mblsplit  25760  voliunlem3  25780  dyadmbl  25828  vitalilem2  25837  vitalilem3  25838  vitalilem4  25839  vitalilem5  25840  vitali  25841  mbff  25853  ismbf  25856  ismbfcn  25857  mbfconst  25861  cncombf  25886  cnmbf  25887  0plef  25900  i1fd  25909  itg1ge0  25914  i1faddlem  25921  i1fmullem  25922  i1fadd  25923  i1fmul  25924  itg1addlem4  25927  i1fmulclem  25930  i1fmulc  25931  itg1mulc  25932  i1fsub  25936  itg1sub  25937  itg1lea  25940  itg1le  25941  mbfi1fseqlem2  25944  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  mbfi1flimlem  25950  mbfmullem2  25952  itg2val  25956  xrge0f  25959  itg2ge0  25963  itg2itg1  25964  itg20  25965  itg2le  25967  itg2const  25968  itg2const2  25969  itg2seq  25970  itg2uba  25971  itg2lea  25972  itg2mulclem  25974  itg2mulc  25975  itg2splitlem  25976  itg2split  25977  itg2monolem1  25978  itg2mono  25981  itg2i1fseqle  25982  itg2i1fseq  25983  itg2addlem  25986  itg2gt0  25988  itg2cnlem1  25989  itg2cnlem2  25990  iblss  26032  i1fibl  26035  itgitg1  26036  itgle  26037  ibladdlem  26047  itgaddlem1  26050  iblabslem  26055  iblabs  26056  iblabsr  26057  iblmulc2  26058  itgmulc2lem1  26059  bddmulibl  26066  bddiblnc  26069  dvnfre  26179  c1liplem1  26223  c1lip2  26225  lhop2  26242  dvcnvrelem2  26245  taylthlem2  26610  dmarea  27194  vmadivsum  27718  rpvmasumlem  27723  mudivsum  27766  selberglem1  27781  selberglem2  27782  selberg2lem  27786  selberg2  27787  pntrsumo1  27801  selbergr  27804  iscgrgd  28855  elee  29350  xrge0tsmsd  33513  nn0omnd  33784  xrge0slmod  33788  raddcn  34439  rrhcn  34507  qqtopn  34521  dmvlsiga  34639  ddeval1  34745  ddeval0  34746  ddemeas  34747  mbfmcnt  34779  sxbrsigalem0  34782  sxbrsigalem3  34783  sxbrsigalem2  34797  isrrvv  34954  dstfrvclim1  34989  signsplypnf  35058  erdsze2lem1  35782  erdsze2lem2  35783  snmlval  35910  knoppcnlem5  37194  knoppcnlem6  37195  knoppcnlem7  37196  knoppcnlem8  37197  cnndvlem2  37235  icoreresf  38106  icoreval  38107  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  poimir  38402  broucube  38403  mblfinlem3  38408  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  ibladdnclem  38425  itgaddnclem1  38427  iblabsnclem  38432  iblabsnc  38433  iblmulc2nc  38434  itgmulc2nclem1  38435  ftc1anclem3  38444  ftc1anclem4  38445  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  filbcmb  38490  rrncmslem  38582  repwsmet  38584  rrnequiv  38585  ismrer1  38588  absex  43115  pell1qrval  43687  pell14qrval  43689  pell1234qrval  43691  k0004ss1  44991  addrval  45288  subrval  45289  mulvval  45290  rpex  46176  climreeq  46443  limsupre  46469  limcresiooub  46470  limcresioolb  46471  limsuppnfdlem  46529  limsuppnflem  46538  limsupmnflem  46548  limsupre2lem  46552  xlimclim  46652  icccncfext  46715  cncfiooicclem1  46721  itgsubsticclem  46803  ovolsplit  46816  dirkerval  46919  dirkercncflem4  46934  fourierdlem14  46949  fourierdlem15  46950  fourierdlem32  46967  fourierdlem33  46968  fourierdlem54  46988  fourierdlem62  46996  fourierdlem70  47004  fourierdlem81  47015  fourierdlem92  47026  fourierdlem102  47036  fourierdlem111  47045  fourierdlem114  47048  etransclem2  47064  rrxtopn0  47121  qndenserrnbllem  47122  qndenserrnbl  47123  qndenserrn  47127  rrnprjdstle  47129  ioorrnopnlem  47132  dmvolsal  47174  hoicvr  47376  hoissrrn  47377  hoiprodcl2  47383  hoicvrrex  47384  ovn0lem  47393  ovn02  47396  hsphoif  47404  hoidmvval  47405  hoissrrn2  47406  hsphoival  47407  hoidmvlelem3  47425  hoidmvle  47428  ovnhoilem1  47429  ovnhoilem2  47430  ovnhoi  47431  hspval  47437  ovnlecvr2  47438  ovncvr2  47439  hoidifhspval2  47443  hoiqssbl  47453  hspmbllem2  47455  hspmbl  47457  hoimbl  47459  opnvonmbllem2  47461  ovolval2lem  47471  ovolval2  47472  ovolval3  47475  ovolval4lem2  47478  ovolval5lem2  47481  ovnovollem1  47484  ovnovollem2  47485  ovnovollem3  47486  vonvolmbllem  47488  vonvolmbl  47489  vitali2  47522  issmflem  47555  incsmf  47570  decsmf  47595  nsssmfmbflem  47606  smfresal  47616  smfmullem4  47622  smf2id  47629  numtowerdt  47734  refdivpm  49474  elbigo2  49482  elbigof  49484  elbigodm  49485  elbigoimp  49486  elbigolo1  49487  prelrrx2  49643  rrx2xpref1o  49648  rrx2xpreen  49649  rrx2linesl  49673  line2  49682  line2x  49684  line2y  49685  crosspcld  50792  veronesematbasd  50813  veroquadmodzerod  50817  veroquadnolindfd  50818  veroquaddetzerod  50819  amgmlemALT  50821