Theorem reex 10617

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10607	. 2 ⊢ ℂ ∈ V
2		ax-resscn 10583	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5190	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ℂcc 10524  ℝcr 10525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  reelprrecn  10618  negfi  11577  xrex  12374  limsuple  14827  limsuplt  14828  limsupbnd1  14831  rlim  14844  rlimf  14850  rlimss  14851  ello12  14865  lo1f  14867  lo1dm  14868  elo12  14876  o1f  14878  o1dm  14879  o1of2  14961  o1rlimmul  14967  o1add2  14972  o1mul2  14973  o1sub2  14974  o1dif  14978  caucvgrlem  15021  fsumo1  15159  rpnnen  15572  cpnnen  15574  ruclem13  15587  ruc  15588  aleph1re  15590  aleph1irr  15591  cnfldds  20101  replusg  20299  remulr  20300  rele2  20303  reds  20305  refldcj  20309  ismet  22930  tngngp2  23258  tngngpd  23259  tngngp  23260  tngngp3  23262  nrmtngnrm  23264  tngnrg  23280  rerest  23409  xrtgioo  23411  xrrest  23412  xrsmopn  23417  opnreen  23436  rectbntr0  23437  xrge0tsms  23439  bcthlem1  23928  bcthlem5  23932  reust  23985  rrxip  23994  rrx0el  24002  ehl0base  24020  ehl1eudis  24024  ehl2eudis  24026  pmltpclem2  24053  ovolficcss  24073  ovolval  24077  elovolmlem  24078  ovolctb2  24096  ismbl  24130  mblsplit  24136  voliunlem3  24156  dyadmbl  24204  vitalilem2  24213  vitalilem3  24214  vitalilem4  24215  vitalilem5  24216  vitali  24217  mbff  24229  ismbf  24232  ismbfcn  24233  mbfconst  24237  cncombf  24262  cnmbf  24263  0plef  24276  i1fd  24285  itg1ge0  24290  i1faddlem  24297  i1fmullem  24298  i1fadd  24299  i1fmul  24300  itg1addlem4  24303  i1fmulclem  24306  i1fmulc  24307  itg1mulc  24308  i1fsub  24312  itg1sub  24313  itg1lea  24316  itg1le  24317  mbfi1fseqlem2  24320  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  mbfi1flimlem  24326  mbfmullem2  24328  itg2val  24332  xrge0f  24335  itg2ge0  24339  itg2itg1  24340  itg20  24341  itg2le  24343  itg2const  24344  itg2const2  24345  itg2seq  24346  itg2uba  24347  itg2lea  24348  itg2mulclem  24350  itg2mulc  24351  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2mono  24357  itg2i1fseqle  24358  itg2i1fseq  24359  itg2addlem  24362  itg2gt0  24364  itg2cnlem1  24365  itg2cnlem2  24366  iblss  24408  i1fibl  24411  itgitg1  24412  itgle  24413  ibladdlem  24423  itgaddlem1  24426  iblabslem  24431  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgmulc2lem1  24435  bddmulibl  24442  bddiblnc  24445  dvnfre  24555  c1liplem1  24599  c1lip2  24601  lhop2  24618  dvcnvrelem2  24621  taylthlem2  24969  dmarea  25543  vmadivsum  26066  rpvmasumlem  26071  mudivsum  26114  selberglem1  26129  selberglem2  26130  selberg2lem  26134  selberg2  26135  pntrsumo1  26149  selbergr  26152  iscgrgd  26307  elee  26688  xrge0tsmsd  30742  nn0omnd  30965  xrge0slmod  30968  raddcn  31282  rrhcn  31348  qqtopn  31362  dmvlsiga  31498  ddeval1  31603  ddeval0  31604  ddemeas  31605  mbfmcnt  31636  sxbrsigalem0  31639  sxbrsigalem3  31640  sxbrsigalem2  31654  isrrvv  31811  dstfrvclim1  31845  signsplypnf  31930  erdsze2lem1  32563  erdsze2lem2  32564  snmlval  32691  knoppcnlem5  33949  knoppcnlem6  33950  knoppcnlem7  33951  knoppcnlem8  33952  cnndvlem2  33990  icoreresf  34769  icoreval  34770  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimir  35090  broucube  35091  mblfinlem3  35096  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ibladdnclem  35113  itgaddnclem1  35115  iblabsnclem  35120  iblabsnc  35121  iblmulc2nc  35122  itgmulc2nclem1  35123  ftc1anclem3  35132  ftc1anclem4  35133  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  filbcmb  35178  rrncmslem  35270  repwsmet  35272  rrnequiv  35273  ismrer1  35276  pell1qrval  39787  pell14qrval  39789  pell1234qrval  39791  k0004ss1  40854  addrval  41170  subrval  41171  mulvval  41172  climreeq  42255  limsupre  42283  limcresiooub  42284  limcresioolb  42285  limsuppnfdlem  42343  limsuppnflem  42352  limsupmnflem  42362  limsupre2lem  42366  xlimclim  42466  icccncfext  42529  cncfiooicclem1  42535  itgsubsticclem  42617  ovolsplit  42630  dirkerval  42733  dirkercncflem4  42748  fourierdlem14  42763  fourierdlem15  42764  fourierdlem32  42781  fourierdlem33  42782  fourierdlem54  42802  fourierdlem62  42810  fourierdlem70  42818  fourierdlem81  42829  fourierdlem92  42840  fourierdlem102  42850  fourierdlem111  42859  fourierdlem114  42862  etransclem2  42878  rrxtopn0  42935  qndenserrnbllem  42936  qndenserrnbl  42937  qndenserrn  42941  rrnprjdstle  42943  ioorrnopnlem  42946  dmvolsal  42986  hoicvr  43187  hoissrrn  43188  hoiprodcl2  43194  hoicvrrex  43195  ovn0lem  43204  ovn02  43207  hsphoif  43215  hoidmvval  43216  hoissrrn2  43217  hsphoival  43218  hoidmvlelem3  43236  hoidmvle  43239  ovnhoilem1  43240  ovnhoilem2  43241  ovnhoi  43242  hspval  43248  ovnlecvr2  43249  ovncvr2  43250  hoidifhspval2  43254  hoiqssbl  43264  hspmbllem2  43266  hspmbl  43268  hoimbl  43270  opnvonmbllem2  43272  ovolval2lem  43282  ovolval2  43283  ovolval3  43286  ovolval4lem2  43289  ovolval5lem2  43292  ovnovollem1  43295  ovnovollem2  43296  ovnovollem3  43297  vonvolmbllem  43299  vonvolmbl  43300  vitali2  43333  issmflem  43361  incsmf  43376  decsmf  43400  nsssmfmbflem  43411  smfresal  43420  smfmullem4  43426  smf2id  43433  refdivpm  44958  elbigo2  44966  elbigof  44968  elbigodm  44969  elbigoimp  44970  elbigolo1  44971  prelrrx2  45127  rrx2xpref1o  45132  rrx2xpreen  45133  rrx2linesl  45157  line2  45166  line2x  45168  line2y  45169  amgmlemALT  45331