Theorem reex 11117

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11107	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11083	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5267	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ℂcc 11024  ℝcr 11025

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  reelprrecn  11118  negfi  12091  xrex  12900  limsuple  15401  limsuplt  15402  limsupbnd1  15405  rlim  15418  rlimf  15424  rlimss  15425  ello12  15439  lo1f  15441  lo1dm  15442  elo12  15450  o1f  15452  o1dm  15453  o1of2  15536  o1rlimmul  15542  o1add2  15547  o1mul2  15548  o1sub2  15549  o1dif  15553  caucvgrlem  15596  fsumo1  15735  rpnnen  16152  cpnnen  16154  ruclem13  16167  ruc  16168  aleph1re  16170  aleph1irr  16171  cnfldds  21321  cnflddsOLD  21334  replusg  21565  remulr  21566  rele2  21569  reds  21571  refldcj  21575  ismet  24267  tngngp2  24596  tngngpd  24597  tngngp  24598  tngngp3  24600  nrmtngnrm  24602  tngnrg  24618  rerest  24748  xrtgioo  24751  xrrest  24752  xrsmopn  24757  opnreen  24776  rectbntr0  24777  xrge0tsms  24779  bcthlem1  25280  bcthlem5  25284  reust  25337  rrxip  25346  rrx0el  25354  ehl0base  25372  ehl1eudis  25376  ehl2eudis  25378  pmltpclem2  25406  ovolficcss  25426  ovolval  25430  elovolmlem  25431  ovolctb2  25449  ismbl  25483  mblsplit  25489  voliunlem3  25509  dyadmbl  25557  vitalilem2  25566  vitalilem3  25567  vitalilem4  25568  vitalilem5  25569  vitali  25570  mbff  25582  ismbf  25585  ismbfcn  25586  mbfconst  25590  cncombf  25615  cnmbf  25616  0plef  25629  i1fd  25638  itg1ge0  25643  i1faddlem  25650  i1fmullem  25651  i1fadd  25652  i1fmul  25653  itg1addlem4  25656  i1fmulclem  25659  i1fmulc  25660  itg1mulc  25661  i1fsub  25665  itg1sub  25666  itg1lea  25669  itg1le  25670  mbfi1fseqlem2  25673  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1flimlem  25679  mbfmullem2  25681  itg2val  25685  xrge0f  25688  itg2ge0  25692  itg2itg1  25693  itg20  25694  itg2le  25696  itg2const  25697  itg2const2  25698  itg2seq  25699  itg2uba  25700  itg2lea  25701  itg2mulclem  25703  itg2mulc  25704  itg2splitlem  25705  itg2split  25706  itg2monolem1  25707  itg2mono  25710  itg2i1fseqle  25711  itg2i1fseq  25712  itg2addlem  25715  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  iblss  25762  i1fibl  25765  itgitg1  25766  itgle  25767  ibladdlem  25777  itgaddlem1  25780  iblabslem  25785  iblabs  25786  iblabsr  25787  iblmulc2  25788  itgmulc2lem1  25789  bddmulibl  25796  bddiblnc  25799  dvnfre  25912  c1liplem1  25957  c1lip2  25959  lhop2  25976  dvcnvrelem2  25979  taylthlem2  26338  taylthlem2OLD  26339  dmarea  26923  vmadivsum  27449  rpvmasumlem  27454  mudivsum  27497  selberglem1  27512  selberglem2  27513  selberg2lem  27517  selberg2  27518  pntrsumo1  27532  selbergr  27535  iscgrgd  28585  elee  28966  xrge0tsmsd  33155  nn0omnd  33425  xrge0slmod  33429  raddcn  34086  rrhcn  34154  qqtopn  34168  dmvlsiga  34286  ddeval1  34391  ddeval0  34392  ddemeas  34393  mbfmcnt  34425  sxbrsigalem0  34428  sxbrsigalem3  34429  sxbrsigalem2  34443  isrrvv  34600  dstfrvclim1  34635  signsplypnf  34707  erdsze2lem1  35397  erdsze2lem2  35398  snmlval  35525  knoppcnlem5  36697  knoppcnlem6  36698  knoppcnlem7  36699  knoppcnlem8  36700  cnndvlem2  36738  icoreresf  37557  icoreval  37558  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  poimir  37854  broucube  37855  mblfinlem3  37860  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  ibladdnclem  37877  itgaddnclem1  37879  iblabsnclem  37884  iblabsnc  37885  iblmulc2nc  37886  itgmulc2nclem1  37887  ftc1anclem3  37896  ftc1anclem4  37897  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  filbcmb  37941  rrncmslem  38033  repwsmet  38035  rrnequiv  38036  ismrer1  38039  absex  42503  pell1qrval  43088  pell14qrval  43090  pell1234qrval  43092  k0004ss1  44392  addrval  44706  subrval  44707  mulvval  44708  rpex  45591  climreeq  45859  limsupre  45885  limcresiooub  45886  limcresioolb  45887  limsuppnfdlem  45945  limsuppnflem  45954  limsupmnflem  45964  limsupre2lem  45968  xlimclim  46068  icccncfext  46131  cncfiooicclem1  46137  itgsubsticclem  46219  ovolsplit  46232  dirkerval  46335  dirkercncflem4  46350  fourierdlem14  46365  fourierdlem15  46366  fourierdlem32  46383  fourierdlem33  46384  fourierdlem54  46404  fourierdlem62  46412  fourierdlem70  46420  fourierdlem81  46431  fourierdlem92  46442  fourierdlem102  46452  fourierdlem111  46461  fourierdlem114  46464  etransclem2  46480  rrxtopn0  46537  qndenserrnbllem  46538  qndenserrnbl  46539  qndenserrn  46543  rrnprjdstle  46545  ioorrnopnlem  46548  dmvolsal  46590  hoicvr  46792  hoissrrn  46793  hoiprodcl2  46799  hoicvrrex  46800  ovn0lem  46809  ovn02  46812  hsphoif  46820  hoidmvval  46821  hoissrrn2  46822  hsphoival  46823  hoidmvlelem3  46841  hoidmvle  46844  ovnhoilem1  46845  ovnhoilem2  46846  ovnhoi  46847  hspval  46853  ovnlecvr2  46854  ovncvr2  46855  hoidifhspval2  46859  hoiqssbl  46869  hspmbllem2  46871  hspmbl  46873  hoimbl  46875  opnvonmbllem2  46877  ovolval2lem  46887  ovolval2  46888  ovolval3  46891  ovolval4lem2  46894  ovolval5lem2  46897  ovnovollem1  46900  ovnovollem2  46901  ovnovollem3  46902  vonvolmbllem  46904  vonvolmbl  46905  vitali2  46938  issmflem  46971  incsmf  46986  decsmf  47011  nsssmfmbflem  47022  smfresal  47032  smfmullem4  47038  smf2id  47045  nthrucw  47130  refdivpm  48790  elbigo2  48798  elbigof  48800  elbigodm  48801  elbigoimp  48802  elbigolo1  48803  prelrrx2  48959  rrx2xpref1o  48964  rrx2xpreen  48965  rrx2linesl  48989  line2  48998  line2x  49000  line2y  49001  amgmlemALT  50048