Theorem reex 11284

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11274	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11250	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5284	1 ⊢ ℝ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11191  ℝcr 11192

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-cnex 11249  ax-resscn 11250

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  reelprrecn  11285  negfi  12259  xrex  13108  limsuple  15638  limsuplt  15639  limsupbnd1  15642  rlim  15655  rlimf  15661  rlimss  15662  ello12  15676  lo1f  15678  lo1dm  15679  elo12  15687  o1f  15689  o1dm  15690  o1of2  15773  o1rlimmul  15779  o1add2  15784  o1mul2  15785  o1sub2  15786  o1dif  15790  caucvgrlem  15833  fsumo1  15972  rpnnen  16388  cpnnen  16390  ruclem13  16403  ruc  16404  aleph1re  16406  aleph1irr  16407  cnfldds  21683  replusg  21909  remulr  21910  rele2  21913  reds  21915  refldcj  21919  ismet  24635  tngngp2  24964  tngngpd  24965  tngngp  24966  tngngp3  24968  nrmtngnrm  24970  tngnrg  24986  rerest  25116  xrtgioo  25119  xrrest  25120  xrsmopn  25125  opnreen  25144  rectbntr0  25145  xrge0tsms  25147  bcthlem1  25638  bcthlem5  25642  reust  25695  rrxip  25704  rrx0el  25712  ehl0base  25730  ehl1eudis  25734  ehl2eudis  25736  pmltpclem2  25763  ovolficcss  25783  ovolval  25787  elovolmlem  25788  ovolctb2  25806  ismbl  25840  mblsplit  25846  voliunlem3  25866  dyadmbl  25914  vitalilem2  25923  vitalilem3  25924  vitalilem4  25925  vitalilem5  25926  vitali  25927  mbff  25939  ismbf  25942  ismbfcn  25943  mbfconst  25947  cncombf  25972  cnmbf  25973  0plef  25986  i1fd  25995  itg1ge0  26000  i1faddlem  26007  i1fmullem  26008  i1fadd  26009  i1fmul  26010  itg1addlem4  26013  i1fmulclem  26016  i1fmulc  26017  itg1mulc  26018  i1fsub  26022  itg1sub  26023  itg1lea  26026  itg1le  26027  mbfi1fseqlem2  26030  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  mbfi1flimlem  26036  mbfmullem2  26038  itg2val  26042  xrge0f  26045  itg2ge0  26049  itg2itg1  26050  itg20  26051  itg2le  26053  itg2const  26054  itg2const2  26055  itg2seq  26056  itg2uba  26057  itg2lea  26058  itg2mulclem  26060  itg2mulc  26061  itg2splitlem  26062  itg2split  26063  itg2monolem1  26064  itg2mono  26067  itg2i1fseqle  26068  itg2i1fseq  26069  itg2addlem  26072  itg2gt0  26074  itg2cnlem1  26075  itg2cnlem2  26076  iblss  26118  i1fibl  26121  itgitg1  26122  itgle  26123  ibladdlem  26133  itgaddlem1  26136  iblabslem  26141  iblabs  26142  iblabsr  26143  iblmulc2  26144  itgmulc2lem1  26145  bddmulibl  26152  bddiblnc  26155  dvnfre  26265  c1liplem1  26309  c1lip2  26311  lhop2  26328  dvcnvrelem2  26331  taylthlem2  26694  dmarea  27278  vmadivsum  27802  rpvmasumlem  27807  mudivsum  27850  selberglem1  27865  selberglem2  27866  selberg2lem  27870  selberg2  27871  pntrsumo1  27885  selbergr  27888  iscgrgd  28969  elee  29464  xrge0tsmsd  33627  nn0omnd  33898  xrge0slmod  33902  raddcn  34554  rrhcn  34622  qqtopn  34636  dmvlsiga  34754  ddeval1  34860  ddeval0  34861  ddemeas  34862  mbfmcnt  34893  sxbrsigalem0  34896  sxbrsigalem3  34897  sxbrsigalem2  34911  isrrvv  35068  dstfrvclim1  35103  signsplypnf  35172  erdsze2lem1  35947  erdsze2lem2  35948  snmlval  36075  knoppcnlem5  37343  knoppcnlem6  37344  knoppcnlem7  37345  knoppcnlem8  37346  cnndvlem2  37384  icoreresf  38255  icoreval  38256  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  poimir  38551  broucube  38552  mblfinlem3  38557  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  ibladdnclem  38574  itgaddnclem1  38576  iblabsnclem  38581  iblabsnc  38582  iblmulc2nc  38583  itgmulc2nclem1  38584  ftc1anclem3  38593  ftc1anclem4  38594  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  filbcmb  38654  rrncmslem  38746  repwsmet  38748  rrnequiv  38749  ismrer1  38752  absex  43279  pell1qrval  43832  pell14qrval  43834  pell1234qrval  43836  k0004ss1  45136  addrval  45433  subrval  45434  mulvval  45435  rpex  46327  climreeq  46594  limsupre  46620  limcresiooub  46621  limcresioolb  46622  limsuppnfdlem  46680  limsuppnflem  46689  limsupmnflem  46699  limsupre2lem  46703  xlimclim  46803  icccncfext  46866  cncfiooicclem1  46872  itgsubsticclem  46954  ovolsplit  46967  dirkerval  47070  dirkercncflem4  47085  fourierdlem14  47100  fourierdlem15  47101  fourierdlem32  47118  fourierdlem33  47119  fourierdlem54  47139  fourierdlem62  47147  fourierdlem70  47155  fourierdlem81  47166  fourierdlem92  47177  fourierdlem102  47187  fourierdlem111  47196  fourierdlem114  47199  etransclem2  47215  rrxtopn0  47272  qndenserrnbllem  47273  qndenserrnbl  47274  qndenserrn  47278  rrnprjdstle  47280  ioorrnopnlem  47283  dmvolsal  47325  hoicvr  47527  hoissrrn  47528  hoiprodcl2  47534  hoicvrrex  47535  ovn0lem  47544  ovn02  47547  hsphoif  47555  hoidmvval  47556  hoissrrn2  47557  hsphoival  47558  hoidmvlelem3  47576  hoidmvle  47579  ovnhoilem1  47580  ovnhoilem2  47581  ovnhoi  47582  hspval  47588  ovnlecvr2  47589  ovncvr2  47590  hoidifhspval2  47594  hoiqssbl  47604  hspmbllem2  47606  hspmbl  47608  hoimbl  47610  opnvonmbllem2  47612  ovolval2lem  47622  ovolval2  47623  ovolval3  47626  ovolval4lem2  47629  ovolval5lem2  47632  ovnovollem1  47635  ovnovollem2  47636  ovnovollem3  47637  vonvolmbllem  47639  vonvolmbl  47640  vitali2  47673  issmflem  47706  incsmf  47721  decsmf  47746  nsssmfmbflem  47757  smfresal  47767  smfmullem4  47773  smf2id  47780  numtowerdt  47885  refdivpm  49625  elbigo2  49633  elbigof  49635  elbigodm  49636  elbigoimp  49637  elbigolo1  49638  prelrrx2  49794  rrx2xpref1o  49799  rrx2xpreen  49800  rrx2linesl  49824  line2  49833  line2x  49835  line2y  49836  crosspcld  50928  veronesematbasd  50949  veroquadmodzerod  50953  veroquadnolindfd  50954  veroquaddetzerod  50955  amgmlemALT  50957