Theorem reex 11202

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11192	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11168	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5295	1 ⊢ ℝ ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ℂcc 11109  ℝcr 11110

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-cnex 11167  ax-resscn 11168

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923

This theorem is used by:  reelprrecn  11203  negfi  12175  xrex  13022  limsuple  15548  limsuplt  15549  limsupbnd1  15552  rlim  15565  rlimf  15571  rlimss  15572  ello12  15586  lo1f  15588  lo1dm  15589  elo12  15597  o1f  15599  o1dm  15600  o1of2  15683  o1rlimmul  15689  o1add2  15694  o1mul2  15695  o1sub2  15696  o1dif  15700  caucvgrlem  15743  fsumo1  15882  rpnnen  16300  cpnnen  16302  ruclem13  16315  ruc  16316  aleph1re  16318  aleph1irr  16319  cnfldds  21563  replusg  21789  remulr  21790  rele2  21793  reds  21795  refldcj  21799  ismet  24509  tngngp2  24838  tngngpd  24839  tngngp  24840  tngngp3  24842  nrmtngnrm  24844  tngnrg  24860  rerest  24990  xrtgioo  24993  xrrest  24994  xrsmopn  24999  opnreen  25018  rectbntr0  25019  xrge0tsms  25021  bcthlem1  25512  bcthlem5  25516  reust  25569  rrxip  25578  rrx0el  25586  ehl0base  25604  ehl1eudis  25608  ehl2eudis  25610  pmltpclem2  25637  ovolficcss  25657  ovolval  25661  elovolmlem  25662  ovolctb2  25680  ismbl  25714  mblsplit  25720  voliunlem3  25740  dyadmbl  25788  vitalilem2  25797  vitalilem3  25798  vitalilem4  25799  vitalilem5  25800  vitali  25801  mbff  25813  ismbf  25816  ismbfcn  25817  mbfconst  25821  cncombf  25846  cnmbf  25847  0plef  25860  i1fd  25869  itg1ge0  25874  i1faddlem  25881  i1fmullem  25882  i1fadd  25883  i1fmul  25884  itg1addlem4  25887  i1fmulclem  25890  i1fmulc  25891  itg1mulc  25892  i1fsub  25896  itg1sub  25897  itg1lea  25900  itg1le  25901  mbfi1fseqlem2  25904  mbfi1fseqlem4  25906  mbfi1fseqlem5  25907  mbfi1flimlem  25910  mbfmullem2  25912  itg2val  25916  xrge0f  25919  itg2ge0  25923  itg2itg1  25924  itg20  25925  itg2le  25927  itg2const  25928  itg2const2  25929  itg2seq  25930  itg2uba  25931  itg2lea  25932  itg2mulclem  25934  itg2mulc  25935  itg2splitlem  25936  itg2split  25937  itg2monolem1  25938  itg2mono  25941  itg2i1fseqle  25942  itg2i1fseq  25943  itg2addlem  25946  itg2gt0  25948  itg2cnlem1  25949  itg2cnlem2  25950  iblss  25993  i1fibl  25996  itgitg1  25997  itgle  25998  ibladdlem  26008  itgaddlem1  26011  iblabslem  26016  iblabs  26017  iblabsr  26018  iblmulc2  26019  itgmulc2lem1  26020  bddmulibl  26027  bddiblnc  26030  dvnfre  26140  c1liplem1  26184  c1lip2  26186  lhop2  26203  dvcnvrelem2  26206  taylthlem2  26566  dmarea  27151  vmadivsum  27675  rpvmasumlem  27680  mudivsum  27723  selberglem1  27738  selberglem2  27739  selberg2lem  27743  selberg2  27744  pntrsumo1  27758  selbergr  27761  iscgrgd  28811  elee  29272  xrge0tsmsd  33416  nn0omnd  33687  xrge0slmod  33691  raddcn  34342  rrhcn  34410  qqtopn  34424  dmvlsiga  34542  ddeval1  34648  ddeval0  34649  ddemeas  34650  mbfmcnt  34682  sxbrsigalem0  34685  sxbrsigalem3  34686  sxbrsigalem2  34700  isrrvv  34857  dstfrvclim1  34892  signsplypnf  34961  erdsze2lem1  35708  erdsze2lem2  35709  snmlval  35836  knoppcnlem5  37119  knoppcnlem6  37120  knoppcnlem7  37121  knoppcnlem8  37122  cnndvlem2  37160  icoreresf  38031  icoreval  38032  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  poimir  38337  broucube  38338  mblfinlem3  38343  itg2addnclem  38355  itg2addnclem3  38357  itg2addnc  38358  itg2gt0cn  38359  ibladdnclem  38360  itgaddnclem1  38362  iblabsnclem  38367  iblabsnc  38368  iblmulc2nc  38369  itgmulc2nclem1  38370  ftc1anclem3  38379  ftc1anclem4  38380  ftc1anclem5  38381  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  filbcmb  38424  rrncmslem  38516  repwsmet  38518  rrnequiv  38519  ismrer1  38522  absex  43049  pell1qrval  43606  pell14qrval  43608  pell1234qrval  43610  k0004ss1  44910  addrval  45207  subrval  45208  mulvval  45209  rpex  46095  climreeq  46362  limsupre  46388  limcresiooub  46389  limcresioolb  46390  limsuppnfdlem  46448  limsuppnflem  46457  limsupmnflem  46467  limsupre2lem  46471  xlimclim  46571  icccncfext  46634  cncfiooicclem1  46640  itgsubsticclem  46722  ovolsplit  46735  dirkerval  46838  dirkercncflem4  46853  fourierdlem14  46868  fourierdlem15  46869  fourierdlem32  46886  fourierdlem33  46887  fourierdlem54  46907  fourierdlem62  46915  fourierdlem70  46923  fourierdlem81  46934  fourierdlem92  46945  fourierdlem102  46955  fourierdlem111  46964  fourierdlem114  46967  etransclem2  46983  rrxtopn0  47040  qndenserrnbllem  47041  qndenserrnbl  47042  qndenserrn  47046  rrnprjdstle  47048  ioorrnopnlem  47051  dmvolsal  47093  hoicvr  47295  hoissrrn  47296  hoiprodcl2  47302  hoicvrrex  47303  ovn0lem  47312  ovn02  47315  hsphoif  47323  hoidmvval  47324  hoissrrn2  47325  hsphoival  47326  hoidmvlelem3  47344  hoidmvle  47347  ovnhoilem1  47348  ovnhoilem2  47349  ovnhoi  47350  hspval  47356  ovnlecvr2  47357  ovncvr2  47358  hoidifhspval2  47362  hoiqssbl  47372  hspmbllem2  47374  hspmbl  47376  hoimbl  47378  opnvonmbllem2  47380  ovolval2lem  47390  ovolval2  47391  ovolval3  47394  ovolval4lem2  47397  ovolval5lem2  47400  ovnovollem1  47403  ovnovollem2  47404  ovnovollem3  47405  vonvolmbllem  47407  vonvolmbl  47408  vitali2  47441  issmflem  47474  incsmf  47489  decsmf  47514  nsssmfmbflem  47525  smfresal  47535  smfmullem4  47541  smf2id  47548  nthrucw  47640  refdivpm  49357  elbigo2  49365  elbigof  49367  elbigodm  49368  elbigoimp  49369  elbigolo1  49370  prelrrx2  49526  rrx2xpref1o  49531  rrx2xpreen  49532  rrx2linesl  49556  line2  49565  line2x  49567  line2y  49568  crosspcli  50674  amgmlemALT  50684