Theorem reex 10622

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10612	. 2 ⊢ ℂ ∈ V
2		ax-resscn 10588	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5218	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3494  ℂcc 10529  ℝcr 10530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-cnex 10587  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951

This theorem is referenced by:  reelprrecn  10623  negfi  11583  xrex  12380  limsuple  14829  limsuplt  14830  limsupbnd1  14833  rlim  14846  rlimf  14852  rlimss  14853  ello12  14867  lo1f  14869  lo1dm  14870  elo12  14878  o1f  14880  o1dm  14881  o1of2  14963  o1rlimmul  14969  o1add2  14974  o1mul2  14975  o1sub2  14976  o1dif  14980  caucvgrlem  15023  fsumo1  15161  rpnnen  15574  cpnnen  15576  ruclem13  15589  ruc  15590  aleph1re  15592  aleph1irr  15593  cnfldds  20549  replusg  20748  remulr  20749  rele2  20752  reds  20754  refldcj  20758  ismet  22927  tngngp2  23255  tngngpd  23256  tngngp  23257  tngngp3  23259  nrmtngnrm  23261  tngnrg  23277  rerest  23406  xrtgioo  23408  xrrest  23409  xrsmopn  23414  opnreen  23433  rectbntr0  23434  xrge0tsms  23436  bcthlem1  23921  bcthlem5  23925  reust  23978  rrxip  23987  rrx0el  23995  ehl0base  24013  ehl1eudis  24017  ehl2eudis  24019  pmltpclem2  24044  ovolficcss  24064  ovolval  24068  elovolmlem  24069  ovolctb2  24087  ismbl  24121  mblsplit  24127  voliunlem3  24147  dyadmbl  24195  vitalilem2  24204  vitalilem3  24205  vitalilem4  24206  vitalilem5  24207  vitali  24208  mbff  24220  ismbf  24223  ismbfcn  24224  mbfconst  24228  cncombf  24253  cnmbf  24254  0plef  24267  i1fd  24276  itg1ge0  24281  i1faddlem  24288  i1fmullem  24289  i1fadd  24290  i1fmul  24291  itg1addlem4  24294  i1fmulclem  24297  i1fmulc  24298  itg1mulc  24299  i1fsub  24303  itg1sub  24304  itg1lea  24307  itg1le  24308  mbfi1fseqlem2  24311  mbfi1fseqlem4  24313  mbfi1fseqlem5  24314  mbfi1flimlem  24317  mbfmullem2  24319  itg2val  24323  xrge0f  24326  itg2ge0  24330  itg2itg1  24331  itg20  24332  itg2le  24334  itg2const  24335  itg2const2  24336  itg2seq  24337  itg2uba  24338  itg2lea  24339  itg2mulclem  24341  itg2mulc  24342  itg2splitlem  24343  itg2split  24344  itg2monolem1  24345  itg2mono  24348  itg2i1fseqle  24349  itg2i1fseq  24350  itg2addlem  24353  itg2gt0  24355  itg2cnlem1  24356  itg2cnlem2  24357  iblss  24399  i1fibl  24402  itgitg1  24403  itgle  24404  ibladdlem  24414  itgaddlem1  24417  iblabslem  24422  iblabs  24423  iblabsr  24424  iblmulc2  24425  itgmulc2lem1  24426  bddmulibl  24433  dvnfre  24543  c1liplem1  24587  c1lip2  24589  lhop2  24606  dvcnvrelem2  24609  taylthlem2  24956  dmarea  25529  vmadivsum  26052  rpvmasumlem  26057  mudivsum  26100  selberglem1  26115  selberglem2  26116  selberg2lem  26120  selberg2  26121  pntrsumo1  26135  selbergr  26138  iscgrgd  26293  elee  26674  xrge0tsmsd  30687  nn0omnd  30909  xrge0slmod  30912  raddcn  31167  rrhcn  31233  qqtopn  31247  dmvlsiga  31383  ddeval1  31488  ddeval0  31489  ddemeas  31490  mbfmcnt  31521  sxbrsigalem0  31524  sxbrsigalem3  31525  sxbrsigalem2  31539  isrrvv  31696  dstfrvclim1  31730  signsplypnf  31815  erdsze2lem1  32445  erdsze2lem2  32446  snmlval  32573  knoppcnlem5  33831  knoppcnlem6  33832  knoppcnlem7  33833  knoppcnlem8  33834  cnndvlem2  33872  icoreresf  34627  icoreval  34628  poimirlem29  34915  poimirlem30  34916  poimirlem31  34917  poimir  34919  broucube  34920  mblfinlem3  34925  itg2addnclem  34937  itg2addnclem3  34939  itg2addnc  34940  itg2gt0cn  34941  ibladdnclem  34942  itgaddnclem1  34944  iblabsnclem  34949  iblabsnc  34950  iblmulc2nc  34951  itgmulc2nclem1  34952  bddiblnc  34956  ftc1anclem3  34963  ftc1anclem4  34964  ftc1anclem5  34965  ftc1anclem6  34966  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  filbcmb  35009  rrncmslem  35104  repwsmet  35106  rrnequiv  35107  ismrer1  35110  pell1qrval  39436  pell14qrval  39438  pell1234qrval  39440  k0004ss1  40494  addrval  40791  subrval  40792  mulvval  40793  climreeq  41887  limsupre  41915  limcresiooub  41916  limcresioolb  41917  limsuppnfdlem  41975  limsuppnflem  41984  limsupmnflem  41994  limsupre2lem  41998  xlimclim  42098  icccncfext  42163  cncfiooicclem1  42169  itgsubsticclem  42253  ovolsplit  42267  dirkerval  42370  dirkercncflem4  42385  fourierdlem14  42400  fourierdlem15  42401  fourierdlem32  42418  fourierdlem33  42419  fourierdlem54  42439  fourierdlem62  42447  fourierdlem70  42455  fourierdlem81  42466  fourierdlem92  42477  fourierdlem102  42487  fourierdlem111  42496  fourierdlem114  42499  etransclem2  42515  rrxtopn0  42572  qndenserrnbllem  42573  qndenserrnbl  42574  qndenserrn  42578  rrnprjdstle  42580  ioorrnopnlem  42583  dmvolsal  42623  hoicvr  42824  hoissrrn  42825  hoiprodcl2  42831  hoicvrrex  42832  ovn0lem  42841  ovn02  42844  hsphoif  42852  hoidmvval  42853  hoissrrn2  42854  hsphoival  42855  hoidmvlelem3  42873  hoidmvle  42876  ovnhoilem1  42877  ovnhoilem2  42878  ovnhoi  42879  hspval  42885  ovnlecvr2  42886  ovncvr2  42887  hoidifhspval2  42891  hoiqssbl  42901  hspmbllem2  42903  hspmbl  42905  hoimbl  42907  opnvonmbllem2  42909  ovolval2lem  42919  ovolval2  42920  ovolval3  42923  ovolval4lem2  42926  ovolval5lem2  42929  ovnovollem1  42932  ovnovollem2  42933  ovnovollem3  42934  vonvolmbllem  42936  vonvolmbl  42937  vitali2  42970  issmflem  42998  incsmf  43013  decsmf  43037  nsssmfmbflem  43048  smfresal  43057  smfmullem4  43063  smf2id  43070  refdivpm  44598  elbigo2  44606  elbigof  44608  elbigodm  44609  elbigoimp  44610  elbigolo1  44611  prelrrx2  44694  rrx2xpref1o  44699  rrx2xpreen  44700  rrx2linesl  44724  line2  44733  line2x  44735  line2y  44736  amgmlemALT  44898