Theorem reex 11135

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11125	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11101	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5272	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ℂcc 11042  ℝcr 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  reelprrecn  11136  negfi  12108  xrex  12922  limsuple  15420  limsuplt  15421  limsupbnd1  15424  rlim  15437  rlimf  15443  rlimss  15444  ello12  15458  lo1f  15460  lo1dm  15461  elo12  15469  o1f  15471  o1dm  15472  o1of2  15555  o1rlimmul  15561  o1add2  15566  o1mul2  15567  o1sub2  15568  o1dif  15572  caucvgrlem  15615  fsumo1  15754  rpnnen  16171  cpnnen  16173  ruclem13  16186  ruc  16187  aleph1re  16189  aleph1irr  16190  cnfldds  21252  cnflddsOLD  21265  replusg  21495  remulr  21496  rele2  21499  reds  21501  refldcj  21505  ismet  24187  tngngp2  24516  tngngpd  24517  tngngp  24518  tngngp3  24520  nrmtngnrm  24522  tngnrg  24538  rerest  24668  xrtgioo  24671  xrrest  24672  xrsmopn  24677  opnreen  24696  rectbntr0  24697  xrge0tsms  24699  bcthlem1  25200  bcthlem5  25204  reust  25257  rrxip  25266  rrx0el  25274  ehl0base  25292  ehl1eudis  25296  ehl2eudis  25298  pmltpclem2  25326  ovolficcss  25346  ovolval  25350  elovolmlem  25351  ovolctb2  25369  ismbl  25403  mblsplit  25409  voliunlem3  25429  dyadmbl  25477  vitalilem2  25486  vitalilem3  25487  vitalilem4  25488  vitalilem5  25489  vitali  25490  mbff  25502  ismbf  25505  ismbfcn  25506  mbfconst  25510  cncombf  25535  cnmbf  25536  0plef  25549  i1fd  25558  itg1ge0  25563  i1faddlem  25570  i1fmullem  25571  i1fadd  25572  i1fmul  25573  itg1addlem4  25576  i1fmulclem  25579  i1fmulc  25580  itg1mulc  25581  i1fsub  25585  itg1sub  25586  itg1lea  25589  itg1le  25590  mbfi1fseqlem2  25593  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  mbfi1flimlem  25599  mbfmullem2  25601  itg2val  25605  xrge0f  25608  itg2ge0  25612  itg2itg1  25613  itg20  25614  itg2le  25616  itg2const  25617  itg2const2  25618  itg2seq  25619  itg2uba  25620  itg2lea  25621  itg2mulclem  25623  itg2mulc  25624  itg2splitlem  25625  itg2split  25626  itg2monolem1  25627  itg2mono  25630  itg2i1fseqle  25631  itg2i1fseq  25632  itg2addlem  25635  itg2gt0  25637  itg2cnlem1  25638  itg2cnlem2  25639  iblss  25682  i1fibl  25685  itgitg1  25686  itgle  25687  ibladdlem  25697  itgaddlem1  25700  iblabslem  25705  iblabs  25706  iblabsr  25707  iblmulc2  25708  itgmulc2lem1  25709  bddmulibl  25716  bddiblnc  25719  dvnfre  25832  c1liplem1  25877  c1lip2  25879  lhop2  25896  dvcnvrelem2  25899  taylthlem2  26258  taylthlem2OLD  26259  dmarea  26843  vmadivsum  27369  rpvmasumlem  27374  mudivsum  27417  selberglem1  27432  selberglem2  27433  selberg2lem  27437  selberg2  27438  pntrsumo1  27452  selbergr  27455  iscgrgd  28416  elee  28797  xrge0tsmsd  32975  nn0omnd  33289  xrge0slmod  33292  raddcn  33892  rrhcn  33960  qqtopn  33974  dmvlsiga  34092  ddeval1  34197  ddeval0  34198  ddemeas  34199  mbfmcnt  34232  sxbrsigalem0  34235  sxbrsigalem3  34236  sxbrsigalem2  34250  isrrvv  34407  dstfrvclim1  34442  signsplypnf  34514  erdsze2lem1  35163  erdsze2lem2  35164  snmlval  35291  knoppcnlem5  36458  knoppcnlem6  36459  knoppcnlem7  36460  knoppcnlem8  36461  cnndvlem2  36499  icoreresf  37313  icoreval  37314  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  poimir  37620  broucube  37621  mblfinlem3  37626  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  itg2gt0cn  37642  ibladdnclem  37643  itgaddnclem1  37645  iblabsnclem  37650  iblabsnc  37651  iblmulc2nc  37652  itgmulc2nclem1  37653  ftc1anclem3  37662  ftc1anclem4  37663  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  filbcmb  37707  rrncmslem  37799  repwsmet  37801  rrnequiv  37802  ismrer1  37805  absex  42209  pell1qrval  42807  pell14qrval  42809  pell1234qrval  42811  k0004ss1  44113  addrval  44428  subrval  44429  mulvval  44430  rpex  45315  climreeq  45584  limsupre  45612  limcresiooub  45613  limcresioolb  45614  limsuppnfdlem  45672  limsuppnflem  45681  limsupmnflem  45691  limsupre2lem  45695  xlimclim  45795  icccncfext  45858  cncfiooicclem1  45864  itgsubsticclem  45946  ovolsplit  45959  dirkerval  46062  dirkercncflem4  46077  fourierdlem14  46092  fourierdlem15  46093  fourierdlem32  46110  fourierdlem33  46111  fourierdlem54  46131  fourierdlem62  46139  fourierdlem70  46147  fourierdlem81  46158  fourierdlem92  46169  fourierdlem102  46179  fourierdlem111  46188  fourierdlem114  46191  etransclem2  46207  rrxtopn0  46264  qndenserrnbllem  46265  qndenserrnbl  46266  qndenserrn  46270  rrnprjdstle  46272  ioorrnopnlem  46275  dmvolsal  46317  hoicvr  46519  hoissrrn  46520  hoiprodcl2  46526  hoicvrrex  46527  ovn0lem  46536  ovn02  46539  hsphoif  46547  hoidmvval  46548  hoissrrn2  46549  hsphoival  46550  hoidmvlelem3  46568  hoidmvle  46571  ovnhoilem1  46572  ovnhoilem2  46573  ovnhoi  46574  hspval  46580  ovnlecvr2  46581  ovncvr2  46582  hoidifhspval2  46586  hoiqssbl  46596  hspmbllem2  46598  hspmbl  46600  hoimbl  46602  opnvonmbllem2  46604  ovolval2lem  46614  ovolval2  46615  ovolval3  46618  ovolval4lem2  46621  ovolval5lem2  46624  ovnovollem1  46627  ovnovollem2  46628  ovnovollem3  46629  vonvolmbllem  46631  vonvolmbl  46632  vitali2  46665  issmflem  46698  incsmf  46713  decsmf  46738  nsssmfmbflem  46749  smfresal  46759  smfmullem4  46765  smf2id  46772  refdivpm  48506  elbigo2  48514  elbigof  48516  elbigodm  48517  elbigoimp  48518  elbigolo1  48519  prelrrx2  48675  rrx2xpref1o  48680  rrx2xpreen  48681  rrx2linesl  48705  line2  48714  line2x  48716  line2y  48717  amgmlemALT  49765