Theorem reex 10971

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10961	. 2 ⊢ ℂ ∈ V
2		ax-resscn 10937	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5247	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3433  ℂcc 10878  ℝcr 10879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-cnex 10936  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  reelprrecn  10972  negfi  11933  xrex  12736  limsuple  15196  limsuplt  15197  limsupbnd1  15200  rlim  15213  rlimf  15219  rlimss  15220  ello12  15234  lo1f  15236  lo1dm  15237  elo12  15245  o1f  15247  o1dm  15248  o1of2  15331  o1rlimmul  15337  o1add2  15342  o1mul2  15343  o1sub2  15344  o1dif  15348  caucvgrlem  15393  fsumo1  15533  rpnnen  15945  cpnnen  15947  ruclem13  15960  ruc  15961  aleph1re  15963  aleph1irr  15964  cnfldds  20616  replusg  20824  remulr  20825  rele2  20828  reds  20830  refldcj  20834  ismet  23485  tngngp2  23825  tngngpd  23826  tngngp  23827  tngngp3  23829  nrmtngnrm  23831  tngnrg  23847  rerest  23976  xrtgioo  23978  xrrest  23979  xrsmopn  23984  opnreen  24003  rectbntr0  24004  xrge0tsms  24006  bcthlem1  24497  bcthlem5  24501  reust  24554  rrxip  24563  rrx0el  24571  ehl0base  24589  ehl1eudis  24593  ehl2eudis  24595  pmltpclem2  24622  ovolficcss  24642  ovolval  24646  elovolmlem  24647  ovolctb2  24665  ismbl  24699  mblsplit  24705  voliunlem3  24725  dyadmbl  24773  vitalilem2  24782  vitalilem3  24783  vitalilem4  24784  vitalilem5  24785  vitali  24786  mbff  24798  ismbf  24801  ismbfcn  24802  mbfconst  24806  cncombf  24831  cnmbf  24832  0plef  24845  i1fd  24854  itg1ge0  24859  i1faddlem  24866  i1fmullem  24867  i1fadd  24868  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulclem  24876  i1fmulc  24877  itg1mulc  24878  i1fsub  24882  itg1sub  24883  itg1lea  24886  itg1le  24887  mbfi1fseqlem2  24890  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1flimlem  24896  mbfmullem2  24898  itg2val  24902  xrge0f  24905  itg2ge0  24909  itg2itg1  24910  itg20  24911  itg2le  24913  itg2const  24914  itg2const2  24915  itg2seq  24916  itg2uba  24917  itg2lea  24918  itg2mulclem  24920  itg2mulc  24921  itg2splitlem  24922  itg2split  24923  itg2monolem1  24924  itg2mono  24927  itg2i1fseqle  24928  itg2i1fseq  24929  itg2addlem  24932  itg2gt0  24934  itg2cnlem1  24935  itg2cnlem2  24936  iblss  24978  i1fibl  24981  itgitg1  24982  itgle  24983  ibladdlem  24993  itgaddlem1  24996  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgmulc2lem1  25005  bddmulibl  25012  bddiblnc  25015  dvnfre  25125  c1liplem1  25169  c1lip2  25171  lhop2  25188  dvcnvrelem2  25191  taylthlem2  25542  dmarea  26116  vmadivsum  26639  rpvmasumlem  26644  mudivsum  26687  selberglem1  26702  selberglem2  26703  selberg2lem  26707  selberg2  26708  pntrsumo1  26722  selbergr  26725  iscgrgd  26883  elee  27271  xrge0tsmsd  31326  nn0omnd  31554  xrge0slmod  31557  raddcn  31888  rrhcn  31956  qqtopn  31970  dmvlsiga  32106  ddeval1  32211  ddeval0  32212  ddemeas  32213  mbfmcnt  32244  sxbrsigalem0  32247  sxbrsigalem3  32248  sxbrsigalem2  32262  isrrvv  32419  dstfrvclim1  32453  signsplypnf  32538  erdsze2lem1  33174  erdsze2lem2  33175  snmlval  33302  knoppcnlem5  34686  knoppcnlem6  34687  knoppcnlem7  34688  knoppcnlem8  34689  cnndvlem2  34727  icoreresf  35532  icoreval  35533  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimir  35819  broucube  35820  mblfinlem3  35825  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  itg2gt0cn  35841  ibladdnclem  35842  itgaddnclem1  35844  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nclem1  35852  ftc1anclem3  35861  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  filbcmb  35907  rrncmslem  35999  repwsmet  36001  rrnequiv  36002  ismrer1  36005  pell1qrval  40675  pell14qrval  40677  pell1234qrval  40679  k0004ss1  41768  addrval  42091  subrval  42092  mulvval  42093  climreeq  43161  limsupre  43189  limcresiooub  43190  limcresioolb  43191  limsuppnfdlem  43249  limsuppnflem  43258  limsupmnflem  43268  limsupre2lem  43272  xlimclim  43372  icccncfext  43435  cncfiooicclem1  43441  itgsubsticclem  43523  ovolsplit  43536  dirkerval  43639  dirkercncflem4  43654  fourierdlem14  43669  fourierdlem15  43670  fourierdlem32  43687  fourierdlem33  43688  fourierdlem54  43708  fourierdlem62  43716  fourierdlem70  43724  fourierdlem81  43735  fourierdlem92  43746  fourierdlem102  43756  fourierdlem111  43765  fourierdlem114  43768  etransclem2  43784  rrxtopn0  43841  qndenserrnbllem  43842  qndenserrnbl  43843  qndenserrn  43847  rrnprjdstle  43849  ioorrnopnlem  43852  dmvolsal  43892  hoicvr  44093  hoissrrn  44094  hoiprodcl2  44100  hoicvrrex  44101  ovn0lem  44110  ovn02  44113  hsphoif  44121  hoidmvval  44122  hoissrrn2  44123  hsphoival  44124  hoidmvlelem3  44142  hoidmvle  44145  ovnhoilem1  44146  ovnhoilem2  44147  ovnhoi  44148  hspval  44154  ovnlecvr2  44155  ovncvr2  44156  hoidifhspval2  44160  hoiqssbl  44170  hspmbllem2  44172  hspmbl  44174  hoimbl  44176  opnvonmbllem2  44178  ovolval2lem  44188  ovolval2  44189  ovolval3  44192  ovolval4lem2  44195  ovolval5lem2  44198  ovnovollem1  44201  ovnovollem2  44202  ovnovollem3  44203  vonvolmbllem  44205  vonvolmbl  44206  vitali2  44239  issmflem  44272  incsmf  44287  decsmf  44312  nsssmfmbflem  44323  smfresal  44333  smfmullem4  44339  smf2id  44346  refdivpm  45901  elbigo2  45909  elbigof  45911  elbigodm  45912  elbigoimp  45913  elbigolo1  45914  prelrrx2  46070  rrx2xpref1o  46075  rrx2xpreen  46076  rrx2linesl  46100  line2  46109  line2x  46111  line2y  46112  amgmlemALT  46518