Theorem reex 11120

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11110	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11086	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5250	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ℂcc 11027  ℝcr 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  reelprrecn  11121  negfi  12096  xrex  12928  limsuple  15431  limsuplt  15432  limsupbnd1  15435  rlim  15448  rlimf  15454  rlimss  15455  ello12  15469  lo1f  15471  lo1dm  15472  elo12  15480  o1f  15482  o1dm  15483  o1of2  15566  o1rlimmul  15572  o1add2  15577  o1mul2  15578  o1sub2  15579  o1dif  15583  caucvgrlem  15626  fsumo1  15766  rpnnen  16185  cpnnen  16187  ruclem13  16200  ruc  16201  aleph1re  16203  aleph1irr  16204  cnfldds  21359  replusg  21585  remulr  21586  rele2  21589  reds  21591  refldcj  21595  ismet  24306  tngngp2  24635  tngngpd  24636  tngngp  24637  tngngp3  24639  nrmtngnrm  24641  tngnrg  24657  rerest  24787  xrtgioo  24790  xrrest  24791  xrsmopn  24796  opnreen  24815  rectbntr0  24816  xrge0tsms  24818  bcthlem1  25309  bcthlem5  25313  reust  25366  rrxip  25375  rrx0el  25383  ehl0base  25401  ehl1eudis  25405  ehl2eudis  25407  pmltpclem2  25434  ovolficcss  25454  ovolval  25458  elovolmlem  25459  ovolctb2  25477  ismbl  25511  mblsplit  25517  voliunlem3  25537  dyadmbl  25585  vitalilem2  25594  vitalilem3  25595  vitalilem4  25596  vitalilem5  25597  vitali  25598  mbff  25610  ismbf  25613  ismbfcn  25614  mbfconst  25618  cncombf  25643  cnmbf  25644  0plef  25657  i1fd  25666  itg1ge0  25671  i1faddlem  25678  i1fmullem  25679  i1fadd  25680  i1fmul  25681  itg1addlem4  25684  i1fmulclem  25687  i1fmulc  25688  itg1mulc  25689  i1fsub  25693  itg1sub  25694  itg1lea  25697  itg1le  25698  mbfi1fseqlem2  25701  mbfi1fseqlem4  25703  mbfi1fseqlem5  25704  mbfi1flimlem  25707  mbfmullem2  25709  itg2val  25713  xrge0f  25716  itg2ge0  25720  itg2itg1  25721  itg20  25722  itg2le  25724  itg2const  25725  itg2const2  25726  itg2seq  25727  itg2uba  25728  itg2lea  25729  itg2mulclem  25731  itg2mulc  25732  itg2splitlem  25733  itg2split  25734  itg2monolem1  25735  itg2mono  25738  itg2i1fseqle  25739  itg2i1fseq  25740  itg2addlem  25743  itg2gt0  25745  itg2cnlem1  25746  itg2cnlem2  25747  iblss  25790  i1fibl  25793  itgitg1  25794  itgle  25795  ibladdlem  25805  itgaddlem1  25808  iblabslem  25813  iblabs  25814  iblabsr  25815  iblmulc2  25816  itgmulc2lem1  25817  bddmulibl  25824  bddiblnc  25827  dvnfre  25937  c1liplem1  25981  c1lip2  25983  lhop2  26000  dvcnvrelem2  26003  taylthlem2  26357  dmarea  26939  vmadivsum  27463  rpvmasumlem  27468  mudivsum  27511  selberglem1  27526  selberglem2  27527  selberg2lem  27531  selberg2  27532  pntrsumo1  27546  selbergr  27549  iscgrgd  28599  elee  28980  xrge0tsmsd  33154  nn0omnd  33427  xrge0slmod  33431  raddcn  34113  rrhcn  34181  qqtopn  34195  dmvlsiga  34313  ddeval1  34418  ddeval0  34419  ddemeas  34420  mbfmcnt  34452  sxbrsigalem0  34455  sxbrsigalem3  34456  sxbrsigalem2  34470  isrrvv  34627  dstfrvclim1  34662  signsplypnf  34734  erdsze2lem1  35431  erdsze2lem2  35432  snmlval  35559  knoppcnlem5  36803  knoppcnlem6  36804  knoppcnlem7  36805  knoppcnlem8  36806  cnndvlem2  36844  icoreresf  37714  icoreval  37715  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimir  38020  broucube  38021  mblfinlem3  38026  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  ibladdnclem  38043  itgaddnclem1  38045  iblabsnclem  38050  iblabsnc  38051  iblmulc2nc  38052  itgmulc2nclem1  38053  ftc1anclem3  38062  ftc1anclem4  38063  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  filbcmb  38107  rrncmslem  38199  repwsmet  38201  rrnequiv  38202  ismrer1  38205  absex  42732  pell1qrval  43291  pell14qrval  43293  pell1234qrval  43295  k0004ss1  44595  addrval  44909  subrval  44910  mulvval  44911  rpex  45791  climreeq  46058  limsupre  46084  limcresiooub  46085  limcresioolb  46086  limsuppnfdlem  46144  limsuppnflem  46153  limsupmnflem  46163  limsupre2lem  46167  xlimclim  46267  icccncfext  46330  cncfiooicclem1  46336  itgsubsticclem  46418  ovolsplit  46431  dirkerval  46534  dirkercncflem4  46549  fourierdlem14  46564  fourierdlem15  46565  fourierdlem32  46582  fourierdlem33  46583  fourierdlem54  46603  fourierdlem62  46611  fourierdlem70  46619  fourierdlem81  46630  fourierdlem92  46641  fourierdlem102  46651  fourierdlem111  46660  fourierdlem114  46663  etransclem2  46679  rrxtopn0  46736  qndenserrnbllem  46737  qndenserrnbl  46738  qndenserrn  46742  rrnprjdstle  46744  ioorrnopnlem  46747  dmvolsal  46789  hoicvr  46991  hoissrrn  46992  hoiprodcl2  46998  hoicvrrex  46999  ovn0lem  47008  ovn02  47011  hsphoif  47019  hoidmvval  47020  hoissrrn2  47021  hsphoival  47022  hoidmvlelem3  47040  hoidmvle  47043  ovnhoilem1  47044  ovnhoilem2  47045  ovnhoi  47046  hspval  47052  ovnlecvr2  47053  ovncvr2  47054  hoidifhspval2  47058  hoiqssbl  47068  hspmbllem2  47070  hspmbl  47072  hoimbl  47074  opnvonmbllem2  47076  ovolval2lem  47086  ovolval2  47087  ovolval3  47090  ovolval4lem2  47093  ovolval5lem2  47096  ovnovollem1  47099  ovnovollem2  47100  ovnovollem3  47101  vonvolmbllem  47103  vonvolmbl  47104  vitali2  47137  issmflem  47170  incsmf  47185  decsmf  47210  nsssmfmbflem  47221  smfresal  47231  smfmullem4  47237  smf2id  47244  nthrucw  47331  refdivpm  49035  elbigo2  49043  elbigof  49045  elbigodm  49046  elbigoimp  49047  elbigolo1  49048  prelrrx2  49204  rrx2xpref1o  49209  rrx2xpreen  49210  rrx2linesl  49234  line2  49243  line2x  49245  line2y  49246  amgmlemALT  50293