Theorem reex 11295

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11285	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11261	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5283	1 ⊢ ℝ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ℂcc 11202  ℝcr 11203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-cnex 11260  ax-resscn 11261

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  reelprrecn  11296  negfi  12270  xrex  13119  limsuple  15651  limsuplt  15652  limsupbnd1  15655  rlim  15668  rlimf  15674  rlimss  15675  ello12  15689  lo1f  15691  lo1dm  15692  elo12  15700  o1f  15702  o1dm  15703  o1of2  15786  o1rlimmul  15792  o1add2  15797  o1mul2  15798  o1sub2  15799  o1dif  15803  caucvgrlem  15846  fsumo1  15985  rpnnen  16401  cpnnen  16403  ruclem13  16416  ruc  16417  aleph1re  16419  aleph1irr  16420  cnfldds  21696  replusg  21922  remulr  21923  rele2  21926  reds  21928  refldcj  21932  ismet  24648  tngngp2  24977  tngngpd  24978  tngngp  24979  tngngp3  24981  nrmtngnrm  24983  tngnrg  24999  rerest  25129  xrtgioo  25132  xrrest  25133  xrsmopn  25138  opnreen  25157  rectbntr0  25158  xrge0tsms  25160  bcthlem1  25651  bcthlem5  25655  reust  25708  rrxip  25717  rrx0el  25725  ehl0base  25743  ehl1eudis  25747  ehl2eudis  25749  pmltpclem2  25776  ovolficcss  25796  ovolval  25800  elovolmlem  25801  ovolctb2  25819  ismbl  25853  mblsplit  25859  voliunlem3  25879  dyadmbl  25927  vitalilem2  25936  vitalilem3  25937  vitalilem4  25938  vitalilem5  25939  vitali  25940  mbff  25952  ismbf  25955  ismbfcn  25956  mbfconst  25960  cncombf  25985  cnmbf  25986  0plef  25999  i1fd  26008  itg1ge0  26013  i1faddlem  26020  i1fmullem  26021  i1fadd  26022  i1fmul  26023  itg1addlem4  26026  i1fmulclem  26029  i1fmulc  26030  itg1mulc  26031  i1fsub  26035  itg1sub  26036  itg1lea  26039  itg1le  26040  mbfi1fseqlem2  26043  mbfi1fseqlem4  26045  mbfi1fseqlem5  26046  mbfi1flimlem  26049  mbfmullem2  26051  itg2val  26055  xrge0f  26058  itg2ge0  26062  itg2itg1  26063  itg20  26064  itg2le  26066  itg2const  26067  itg2const2  26068  itg2seq  26069  itg2uba  26070  itg2lea  26071  itg2mulclem  26073  itg2mulc  26074  itg2splitlem  26075  itg2split  26076  itg2monolem1  26077  itg2mono  26080  itg2i1fseqle  26081  itg2i1fseq  26082  itg2addlem  26085  itg2gt0  26087  itg2cnlem1  26088  itg2cnlem2  26089  iblss  26131  i1fibl  26134  itgitg1  26135  itgle  26136  ibladdlem  26146  itgaddlem1  26149  iblabslem  26154  iblabs  26155  iblabsr  26156  iblmulc2  26157  itgmulc2lem1  26158  bddmulibl  26165  bddiblnc  26168  dvnfre  26278  c1liplem1  26322  c1lip2  26324  lhop2  26341  dvcnvrelem2  26344  taylthlem2  26707  dmarea  27291  vmadivsum  27815  rpvmasumlem  27820  mudivsum  27863  selberglem1  27878  selberglem2  27879  selberg2lem  27883  selberg2  27884  pntrsumo1  27898  selbergr  27901  iscgrgd  28982  elee  29477  xrge0tsmsd  33681  nn0omnd  33952  xrge0slmod  33956  raddcn  34608  rrhcn  34676  qqtopn  34690  dmvlsiga  34808  ddeval1  34914  ddeval0  34915  ddemeas  34916  mbfmcnt  34947  sxbrsigalem0  34950  sxbrsigalem3  34951  sxbrsigalem2  34965  isrrvv  35122  dstfrvclim1  35157  signsplypnf  35226  erdsze2lem1  36055  erdsze2lem2  36056  snmlval  36183  knoppcnlem5  37456  knoppcnlem6  37457  knoppcnlem7  37458  knoppcnlem8  37459  cnndvlem2  37497  icoreresf  38369  icoreval  38370  poimirlem29  38661  poimirlem30  38662  poimirlem31  38663  poimir  38665  broucube  38666  mblfinlem3  38671  itg2addnclem  38683  itg2addnclem3  38685  itg2addnc  38686  itg2gt0cn  38687  ibladdnclem  38688  itgaddnclem1  38690  iblabsnclem  38695  iblabsnc  38696  iblmulc2nc  38697  itgmulc2nclem1  38698  ftc1anclem3  38707  ftc1anclem4  38708  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  filbcmb  38768  rrncmslem  38860  repwsmet  38862  rrnequiv  38863  ismrer1  38866  absex  43393  pell1qrval  43947  pell14qrval  43949  pell1234qrval  43951  k0004ss1  45245  addrval  45542  subrval  45543  mulvval  45544  rpex  46452  climreeq  46719  limsupre  46745  limcresiooub  46746  limcresioolb  46747  limsuppnfdlem  46805  limsuppnflem  46814  limsupmnflem  46824  limsupre2lem  46828  xlimclim  46928  icccncfext  46991  cncfiooicclem1  46997  itgsubsticclem  47079  ovolsplit  47092  dirkerval  47195  dirkercncflem4  47210  fourierdlem14  47225  fourierdlem15  47226  fourierdlem32  47243  fourierdlem33  47244  fourierdlem54  47264  fourierdlem62  47272  fourierdlem70  47280  fourierdlem81  47291  fourierdlem92  47302  fourierdlem102  47312  fourierdlem111  47321  fourierdlem114  47324  etransclem2  47340  rrxtopn0  47397  qndenserrnbllem  47398  qndenserrnbl  47399  qndenserrn  47403  rrnprjdstle  47405  ioorrnopnlem  47408  dmvolsal  47450  hoicvr  47652  hoissrrn  47653  hoiprodcl2  47659  hoicvrrex  47660  ovn0lem  47669  ovn02  47672  hsphoif  47680  hoidmvval  47681  hoissrrn2  47682  hsphoival  47683  hoidmvlelem3  47701  hoidmvle  47704  ovnhoilem1  47705  ovnhoilem2  47706  ovnhoi  47707  hspval  47713  ovnlecvr2  47714  ovncvr2  47715  hoidifhspval2  47719  hoiqssbl  47729  hspmbllem2  47731  hspmbl  47733  hoimbl  47735  opnvonmbllem2  47737  ovolval2lem  47747  ovolval2  47748  ovolval3  47751  ovolval4lem2  47754  ovolval5lem2  47757  ovnovollem1  47760  ovnovollem2  47761  ovnovollem3  47762  vonvolmbllem  47764  vonvolmbl  47765  vitali2  47798  issmflem  47831  incsmf  47846  decsmf  47871  nsssmfmbflem  47882  smfresal  47892  smfmullem4  47898  smf2id  47905  numtowerdt  48010  refdivpm  49750  elbigo2  49758  elbigof  49760  elbigodm  49761  elbigoimp  49762  elbigolo1  49763  prelrrx2  49919  prelrrx2bd  49920  rrx2xpreen  49926  line2  49958  line2x  49960  line2y  49961  crosspcld  51128  veronesematbasd  51149  veroquadmodzerod  51153  veroquadnolindfd  51154  veroquaddetzerod  51155  amgmlemALT  51157