Theorem reex 10893

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10883	. 2 ⊢ ℂ ∈ V
2		ax-resscn 10859	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5241	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800  ℝcr 10801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  reelprrecn  10894  negfi  11854  xrex  12656  limsuple  15115  limsuplt  15116  limsupbnd1  15119  rlim  15132  rlimf  15138  rlimss  15139  ello12  15153  lo1f  15155  lo1dm  15156  elo12  15164  o1f  15166  o1dm  15167  o1of2  15250  o1rlimmul  15256  o1add2  15261  o1mul2  15262  o1sub2  15263  o1dif  15267  caucvgrlem  15312  fsumo1  15452  rpnnen  15864  cpnnen  15866  ruclem13  15879  ruc  15880  aleph1re  15882  aleph1irr  15883  cnfldds  20520  replusg  20727  remulr  20728  rele2  20731  reds  20733  refldcj  20737  ismet  23384  tngngp2  23722  tngngpd  23723  tngngp  23724  tngngp3  23726  nrmtngnrm  23728  tngnrg  23744  rerest  23873  xrtgioo  23875  xrrest  23876  xrsmopn  23881  opnreen  23900  rectbntr0  23901  xrge0tsms  23903  bcthlem1  24393  bcthlem5  24397  reust  24450  rrxip  24459  rrx0el  24467  ehl0base  24485  ehl1eudis  24489  ehl2eudis  24491  pmltpclem2  24518  ovolficcss  24538  ovolval  24542  elovolmlem  24543  ovolctb2  24561  ismbl  24595  mblsplit  24601  voliunlem3  24621  dyadmbl  24669  vitalilem2  24678  vitalilem3  24679  vitalilem4  24680  vitalilem5  24681  vitali  24682  mbff  24694  ismbf  24697  ismbfcn  24698  mbfconst  24702  cncombf  24727  cnmbf  24728  0plef  24741  i1fd  24750  itg1ge0  24755  i1faddlem  24762  i1fmullem  24763  i1fadd  24764  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulclem  24772  i1fmulc  24773  itg1mulc  24774  i1fsub  24778  itg1sub  24779  itg1lea  24782  itg1le  24783  mbfi1fseqlem2  24786  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1flimlem  24792  mbfmullem2  24794  itg2val  24798  xrge0f  24801  itg2ge0  24805  itg2itg1  24806  itg20  24807  itg2le  24809  itg2const  24810  itg2const2  24811  itg2seq  24812  itg2uba  24813  itg2lea  24814  itg2mulclem  24816  itg2mulc  24817  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2mono  24823  itg2i1fseqle  24824  itg2i1fseq  24825  itg2addlem  24828  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  iblss  24874  i1fibl  24877  itgitg1  24878  itgle  24879  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  iblabs  24898  iblabsr  24899  iblmulc2  24900  itgmulc2lem1  24901  bddmulibl  24908  bddiblnc  24911  dvnfre  25021  c1liplem1  25065  c1lip2  25067  lhop2  25084  dvcnvrelem2  25087  taylthlem2  25438  dmarea  26012  vmadivsum  26535  rpvmasumlem  26540  mudivsum  26583  selberglem1  26598  selberglem2  26599  selberg2lem  26603  selberg2  26604  pntrsumo1  26618  selbergr  26621  iscgrgd  26778  elee  27165  xrge0tsmsd  31219  nn0omnd  31447  xrge0slmod  31450  raddcn  31781  rrhcn  31847  qqtopn  31861  dmvlsiga  31997  ddeval1  32102  ddeval0  32103  ddemeas  32104  mbfmcnt  32135  sxbrsigalem0  32138  sxbrsigalem3  32139  sxbrsigalem2  32153  isrrvv  32310  dstfrvclim1  32344  signsplypnf  32429  erdsze2lem1  33065  erdsze2lem2  33066  snmlval  33193  knoppcnlem5  34604  knoppcnlem6  34605  knoppcnlem7  34606  knoppcnlem8  34607  cnndvlem2  34645  icoreresf  35450  icoreval  35451  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimir  35737  broucube  35738  mblfinlem3  35743  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nclem1  35770  ftc1anclem3  35779  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  filbcmb  35825  rrncmslem  35917  repwsmet  35919  rrnequiv  35920  ismrer1  35923  pell1qrval  40584  pell14qrval  40586  pell1234qrval  40588  k0004ss1  41650  addrval  41973  subrval  41974  mulvval  41975  climreeq  43044  limsupre  43072  limcresiooub  43073  limcresioolb  43074  limsuppnfdlem  43132  limsuppnflem  43141  limsupmnflem  43151  limsupre2lem  43155  xlimclim  43255  icccncfext  43318  cncfiooicclem1  43324  itgsubsticclem  43406  ovolsplit  43419  dirkerval  43522  dirkercncflem4  43537  fourierdlem14  43552  fourierdlem15  43553  fourierdlem32  43570  fourierdlem33  43571  fourierdlem54  43591  fourierdlem62  43599  fourierdlem70  43607  fourierdlem81  43618  fourierdlem92  43629  fourierdlem102  43639  fourierdlem111  43648  fourierdlem114  43651  etransclem2  43667  rrxtopn0  43724  qndenserrnbllem  43725  qndenserrnbl  43726  qndenserrn  43730  rrnprjdstle  43732  ioorrnopnlem  43735  dmvolsal  43775  hoicvr  43976  hoissrrn  43977  hoiprodcl2  43983  hoicvrrex  43984  ovn0lem  43993  ovn02  43996  hsphoif  44004  hoidmvval  44005  hoissrrn2  44006  hsphoival  44007  hoidmvlelem3  44025  hoidmvle  44028  ovnhoilem1  44029  ovnhoilem2  44030  ovnhoi  44031  hspval  44037  ovnlecvr2  44038  ovncvr2  44039  hoidifhspval2  44043  hoiqssbl  44053  hspmbllem2  44055  hspmbl  44057  hoimbl  44059  opnvonmbllem2  44061  ovolval2lem  44071  ovolval2  44072  ovolval3  44075  ovolval4lem2  44078  ovolval5lem2  44081  ovnovollem1  44084  ovnovollem2  44085  ovnovollem3  44086  vonvolmbllem  44088  vonvolmbl  44089  vitali2  44122  issmflem  44150  incsmf  44165  decsmf  44189  nsssmfmbflem  44200  smfresal  44209  smfmullem4  44215  smf2id  44222  refdivpm  45778  elbigo2  45786  elbigof  45788  elbigodm  45789  elbigoimp  45790  elbigolo1  45791  prelrrx2  45947  rrx2xpref1o  45952  rrx2xpreen  45953  rrx2linesl  45977  line2  45986  line2x  45988  line2y  45989  amgmlemALT  46393