Theorem reex 10027

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10017	. 2 ⊢ ℂ ∈ V
2		ax-resscn 9993	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 4803	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200  ℂcc 9934  ℝcr 9935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  reelprrecn  10028  negfi  10971  xrex  11829  limsuple  14209  limsuplt  14210  limsupbnd1  14213  rlim  14226  rlimf  14232  rlimss  14233  ello12  14247  lo1f  14249  lo1dm  14250  elo12  14258  o1f  14260  o1dm  14261  o1of2  14343  o1rlimmul  14349  o1add2  14354  o1mul2  14355  o1sub2  14356  o1dif  14360  caucvgrlem  14403  fsumo1  14544  rpnnen  14956  cpnnen  14958  ruclem13  14971  ruc  14972  aleph1re  14974  aleph1irr  14975  cnfldds  19756  replusg  19956  remulr  19957  rele2  19960  reds  19962  refldcj  19966  ismet  22128  tngngp2  22456  tngngpd  22457  tngngp  22458  tngngp3  22460  nrmtngnrm  22462  tngnrg  22478  rerest  22607  xrtgioo  22609  xrrest  22610  xrsmopn  22615  opnreen  22634  rectbntr0  22635  xrge0tsms  22637  bcthlem1  23121  bcthlem5  23125  reust  23169  rrxip  23178  pmltpclem2  23218  ovolficcss  23238  ovolval  23242  elovolm  23243  elovolmr  23244  ovolmge0  23245  ovolgelb  23248  ovolctb2  23260  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovolshftlem2  23278  ovolicc2  23290  ismbl  23294  mblsplit  23300  voliunlem3  23320  ioombl1  23330  dyadmbl  23368  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  vitalilem5  23381  vitali  23382  mbff  23394  ismbf  23397  ismbfcn  23398  mbfconst  23402  cncombf  23425  cnmbf  23426  0plef  23439  i1fd  23448  itg1ge0  23453  i1faddlem  23460  i1fmullem  23461  i1fadd  23462  i1fmul  23463  itg1addlem4  23466  i1fmulclem  23469  i1fmulc  23470  itg1mulc  23471  i1fsub  23475  itg1sub  23476  itg1lea  23479  itg1le  23480  mbfi1fseqlem2  23483  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1flimlem  23489  mbfmullem2  23491  itg2val  23495  xrge0f  23498  itg2ge0  23502  itg2itg1  23503  itg20  23504  itg2le  23506  itg2const  23507  itg2const2  23508  itg2seq  23509  itg2uba  23510  itg2lea  23511  itg2mulclem  23513  itg2mulc  23514  itg2splitlem  23515  itg2split  23516  itg2monolem1  23517  itg2mono  23520  itg2i1fseqle  23521  itg2i1fseq  23522  itg2addlem  23525  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  iblss  23571  i1fibl  23574  itgitg1  23575  itgle  23576  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  itgmulc2lem1  23598  bddmulibl  23605  dvnfre  23715  c1liplem1  23759  c1lip2  23761  lhop2  23778  dvcnvrelem2  23781  taylthlem2  24128  dmarea  24684  vmadivsum  25171  rpvmasumlem  25176  mudivsum  25219  selberglem1  25234  selberglem2  25235  selberg2lem  25239  selberg2  25240  pntrsumo1  25254  selbergr  25257  iscgrgd  25408  elee  25774  xrge0tsmsd  29785  nn0omnd  29841  xrge0slmod  29844  raddcn  29975  rrhcn  30041  qqtopn  30055  dmvlsiga  30192  ddeval1  30297  ddeval0  30298  ddemeas  30299  mbfmcnt  30330  sxbrsigalem0  30333  sxbrsigalem3  30334  sxbrsigalem2  30348  isrrvv  30505  dstfrvclim1  30539  signsplypnf  30627  erdsze2lem1  31185  erdsze2lem2  31186  snmlval  31313  knoppcnlem5  32487  knoppcnlem6  32488  knoppcnlem7  32489  knoppcnlem8  32490  cnndvlem2  32529  icoreresf  33200  icoreval  33201  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimir  33442  broucube  33443  mblfinlem3  33448  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  itgmulc2nclem1  33476  bddiblnc  33480  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  filbcmb  33535  rrncmslem  33631  repwsmet  33633  rrnequiv  33634  ismrer1  33637  pell1qrval  37410  pell14qrval  37412  pell1234qrval  37414  k0004ss1  38449  addrval  38670  subrval  38671  mulvval  38672  climreeq  39845  limsupre  39873  limcresiooub  39874  limcresioolb  39875  limsuppnfdlem  39933  limsuppnflem  39942  limsupmnflem  39952  limsupre2lem  39956  xlimclim  40050  icccncfext  40100  cncfiooicclem1  40106  itgsubsticclem  40191  ovolsplit  40205  dirkerval  40308  dirkercncflem4  40323  fourierdlem14  40338  fourierdlem15  40339  fourierdlem32  40356  fourierdlem33  40357  fourierdlem54  40377  fourierdlem62  40385  fourierdlem70  40393  fourierdlem81  40404  fourierdlem92  40415  fourierdlem102  40425  fourierdlem111  40434  fourierdlem114  40437  etransclem2  40453  rrxtopn0  40513  qndenserrnbllem  40514  qndenserrnbl  40515  qndenserrn  40519  rrnprjdstle  40521  ioorrnopnlem  40524  dmvolsal  40564  hoicvr  40762  hoissrrn  40763  hoiprodcl2  40769  hoicvrrex  40770  ovn0lem  40779  ovn02  40782  hsphoif  40790  hoidmvval  40791  hoissrrn2  40792  hsphoival  40793  hoidmvlelem3  40811  hoidmvle  40814  ovnhoilem1  40815  ovnhoilem2  40816  ovnhoi  40817  hspval  40823  ovnlecvr2  40824  ovncvr2  40825  hoidifhspval2  40829  hoiqssbl  40839  hspmbllem2  40841  hspmbl  40843  hoimbl  40845  opnvonmbllem2  40847  ovolval2lem  40857  ovolval2  40858  ovolval3  40861  ovolval4lem2  40864  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  ovnovollem3  40872  vonvolmbllem  40874  vonvolmbl  40875  vitali2  40908  issmflem  40936  incsmf  40951  decsmf  40975  nsssmfmbflem  40986  smfresal  40995  smfmullem4  41001  smf2id  41008  refdivpm  42338  elbigo2  42346  elbigof  42348  elbigodm  42349  elbigoimp  42350  elbigolo1  42351  amgmlemALT  42549