Theorem reex 11328

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11318	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11294	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5289	1 ⊢ ℝ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11235  ℝcr 11236

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-cnex 11293  ax-resscn 11294

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  reelprrecn  11329  negfi  12304  xrex  13153  limsuple  15686  limsuplt  15687  limsupbnd1  15690  rlim  15703  rlimf  15709  rlimss  15710  ello12  15724  lo1f  15726  lo1dm  15727  elo12  15735  o1f  15737  o1dm  15738  o1of2  15821  o1rlimmul  15827  o1add2  15832  o1mul2  15833  o1sub2  15834  o1dif  15838  caucvgrlem  15881  fsumo1  16020  rpnnen  16436  cpnnen  16438  ruclem13  16451  ruc  16452  aleph1re  16454  aleph1irr  16455  cnfldds  21732  replusg  21960  remulr  21961  rele2  21964  reds  21966  refldcj  21970  ismet  24686  tngngp2  25015  tngngpd  25016  tngngp  25017  tngngp3  25019  nrmtngnrm  25021  tngnrg  25037  rerest  25167  xrtgioo  25170  xrrest  25171  xrsmopn  25176  opnreen  25195  rectbntr0  25196  xrge0tsms  25198  bcthlem1  25689  bcthlem5  25693  reust  25746  rrxip  25755  rrx0el  25763  ehl0base  25781  ehl1eudis  25785  ehl2eudis  25787  pmltpclem2  25814  ovolficcss  25834  ovolval  25838  elovolmlem  25839  ovolctb2  25857  ismbl  25891  mblsplit  25897  voliunlem3  25917  dyadmbl  25965  vitalilem2  25974  vitalilem3  25975  vitalilem4  25976  vitalilem5  25977  vitali  25978  mbff  25990  ismbf  25993  ismbfcn  25994  mbfconst  25998  cncombf  26023  cnmbf  26024  0plef  26037  i1fd  26046  itg1ge0  26051  i1faddlem  26058  i1fmullem  26059  i1fadd  26060  i1fmul  26061  itg1addlem4  26064  i1fmulclem  26067  i1fmulc  26068  itg1mulc  26069  i1fsub  26073  itg1sub  26074  itg1lea  26077  itg1le  26078  mbfi1fseqlem2  26081  mbfi1fseqlem4  26083  mbfi1fseqlem5  26084  mbfi1flimlem  26087  mbfmullem2  26089  itg2val  26093  xrge0f  26096  itg2ge0  26100  itg2itg1  26101  itg20  26102  itg2le  26104  itg2const  26105  itg2const2  26106  itg2seq  26107  itg2uba  26108  itg2lea  26109  itg2mulclem  26111  itg2mulc  26112  itg2splitlem  26113  itg2split  26114  itg2monolem1  26115  itg2mono  26118  itg2i1fseqle  26119  itg2i1fseq  26120  itg2addlem  26123  itg2gt0  26125  itg2cnlem1  26126  itg2cnlem2  26127  iblss  26169  i1fibl  26172  itgitg1  26173  itgle  26174  ibladdlem  26184  itgaddlem1  26187  iblabslem  26192  iblabs  26193  iblabsr  26194  iblmulc2  26195  itgmulc2lem1  26196  bddmulibl  26203  bddiblnc  26206  dvnfre  26316  c1liplem1  26360  c1lip2  26362  lhop2  26379  dvcnvrelem2  26382  taylthlem2  26747  dmarea  27331  vmadivsum  27855  rpvmasumlem  27860  mudivsum  27903  selberglem1  27918  selberglem2  27919  selberg2lem  27923  selberg2  27924  pntrsumo1  27938  selbergr  27941  iscgrgd  29022  elee  29517  xrge0tsmsd  33723  nn0omnd  34002  xrge0slmod  34006  raddcn  34665  rrhcn  34733  qqtopn  34747  dmvlsiga  34865  ddeval1  34971  ddeval0  34972  ddemeas  34973  mbfmcnt  35004  sxbrsigalem0  35007  sxbrsigalem3  35008  sxbrsigalem2  35022  isrrvv  35179  dstfrvclim1  35214  signsplypnf  35283  erdsze2lem1  36169  erdsze2lem2  36170  snmlval  36297  knoppcnlem5  37571  knoppcnlem6  37572  knoppcnlem7  37573  knoppcnlem8  37574  cnndvlem2  37612  icoreresf  38536  icoreval  38537  poimirlem29  38828  poimirlem30  38829  poimirlem31  38830  poimir  38832  broucube  38833  mblfinlem3  38838  itg2addnclem  38850  itg2addnclem3  38852  itg2addnc  38853  itg2gt0cn  38854  ibladdnclem  38855  itgaddnclem1  38857  iblabsnclem  38862  iblabsnc  38863  iblmulc2nc  38864  itgmulc2nclem1  38865  ftc1anclem3  38874  ftc1anclem4  38875  ftc1anclem5  38876  ftc1anclem6  38877  ftc1anclem7  38878  ftc1anclem8  38879  ftc1anc  38880  filbcmb  38933  rrncmslem  39025  repwsmet  39027  rrnequiv  39028  ismrer1  39031  absex  43559  pell1qrval  44113  pell14qrval  44115  pell1234qrval  44117  k0004ss1  45406  addrval  45702  subrval  45703  mulvval  45704  rpex  46625  climreeq  46892  limsupre  46918  limcresiooub  46919  limcresioolb  46920  limsuppnfdlem  46978  limsuppnflem  46987  limsupmnflem  46997  limsupre2lem  47001  xlimclim  47101  icccncfext  47164  cncfiooicclem1  47170  itgsubsticclem  47252  ovolsplit  47265  dirkerval  47368  dirkercncflem4  47383  fourierdlem14  47398  fourierdlem15  47399  fourierdlem32  47416  fourierdlem33  47417  fourierdlem54  47437  fourierdlem62  47445  fourierdlem70  47453  fourierdlem81  47464  fourierdlem92  47475  fourierdlem102  47485  fourierdlem111  47494  fourierdlem114  47497  etransclem2  47513  rrxtopn0  47570  qndenserrnbllem  47571  qndenserrnbl  47572  qndenserrn  47576  rrnprjdstle  47578  ioorrnopnlem  47581  dmvolsal  47623  hoicvr  47825  hoissrrn  47826  hoiprodcl2  47832  hoicvrrex  47833  ovn0lem  47842  ovn02  47845  hsphoif  47853  hoidmvval  47854  hoissrrn2  47855  hsphoival  47856  hoidmvlelem3  47874  hoidmvle  47877  ovnhoilem1  47878  ovnhoilem2  47879  ovnhoi  47880  hspval  47886  ovnlecvr2  47887  ovncvr2  47888  hoidifhspval2  47892  hoiqssbl  47902  hspmbllem2  47904  hspmbl  47906  hoimbl  47908  opnvonmbllem2  47910  ovolval2lem  47920  ovolval2  47921  ovolval3  47924  ovolval4lem2  47927  ovolval5lem2  47930  ovnovollem1  47933  ovnovollem2  47934  ovnovollem3  47935  vonvolmbllem  47937  vonvolmbl  47938  vitali2  47971  issmflem  48004  incsmf  48019  decsmf  48044  nsssmfmbflem  48055  smfresal  48065  smfmullem4  48071  smf2id  48078  numtowerdt  48183  refdivpm  49981  elbigo2  49989  elbigof  49991  elbigodm  49992  elbigoimp  49993  elbigolo1  49994  prelrrx2  50150  prelrrx2bd  50151  rrx2xpreen  50157  line2  50189  line2x  50191  line2y  50192  crosspcld  51381  veronesematbasd  51402  veroquadmodzerod  51406  veroquadnolindfd  51407  veroquaddetzerod  51408  amgmlemALT  51410