Theorem reex 11097

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11087	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11063	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5260	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ℂcc 11004  ℝcr 11005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-cnex 11062  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3909  df-ss 3919

This theorem is referenced by:  reelprrecn  11098  negfi  12071  xrex  12885  limsuple  15385  limsuplt  15386  limsupbnd1  15389  rlim  15402  rlimf  15408  rlimss  15409  ello12  15423  lo1f  15425  lo1dm  15426  elo12  15434  o1f  15436  o1dm  15437  o1of2  15520  o1rlimmul  15526  o1add2  15531  o1mul2  15532  o1sub2  15533  o1dif  15537  caucvgrlem  15580  fsumo1  15719  rpnnen  16136  cpnnen  16138  ruclem13  16151  ruc  16152  aleph1re  16154  aleph1irr  16155  cnfldds  21304  cnflddsOLD  21317  replusg  21548  remulr  21549  rele2  21552  reds  21554  refldcj  21558  ismet  24239  tngngp2  24568  tngngpd  24569  tngngp  24570  tngngp3  24572  nrmtngnrm  24574  tngnrg  24590  rerest  24720  xrtgioo  24723  xrrest  24724  xrsmopn  24729  opnreen  24748  rectbntr0  24749  xrge0tsms  24751  bcthlem1  25252  bcthlem5  25256  reust  25309  rrxip  25318  rrx0el  25326  ehl0base  25344  ehl1eudis  25348  ehl2eudis  25350  pmltpclem2  25378  ovolficcss  25398  ovolval  25402  elovolmlem  25403  ovolctb2  25421  ismbl  25455  mblsplit  25461  voliunlem3  25481  dyadmbl  25529  vitalilem2  25538  vitalilem3  25539  vitalilem4  25540  vitalilem5  25541  vitali  25542  mbff  25554  ismbf  25557  ismbfcn  25558  mbfconst  25562  cncombf  25587  cnmbf  25588  0plef  25601  i1fd  25610  itg1ge0  25615  i1faddlem  25622  i1fmullem  25623  i1fadd  25624  i1fmul  25625  itg1addlem4  25628  i1fmulclem  25631  i1fmulc  25632  itg1mulc  25633  i1fsub  25637  itg1sub  25638  itg1lea  25641  itg1le  25642  mbfi1fseqlem2  25645  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1flimlem  25651  mbfmullem2  25653  itg2val  25657  xrge0f  25660  itg2ge0  25664  itg2itg1  25665  itg20  25666  itg2le  25668  itg2const  25669  itg2const2  25670  itg2seq  25671  itg2uba  25672  itg2lea  25673  itg2mulclem  25675  itg2mulc  25676  itg2splitlem  25677  itg2split  25678  itg2monolem1  25679  itg2mono  25682  itg2i1fseqle  25683  itg2i1fseq  25684  itg2addlem  25687  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  iblss  25734  i1fibl  25737  itgitg1  25738  itgle  25739  ibladdlem  25749  itgaddlem1  25752  iblabslem  25757  iblabs  25758  iblabsr  25759  iblmulc2  25760  itgmulc2lem1  25761  bddmulibl  25768  bddiblnc  25771  dvnfre  25884  c1liplem1  25929  c1lip2  25931  lhop2  25948  dvcnvrelem2  25951  taylthlem2  26310  taylthlem2OLD  26311  dmarea  26895  vmadivsum  27421  rpvmasumlem  27426  mudivsum  27469  selberglem1  27484  selberglem2  27485  selberg2lem  27489  selberg2  27490  pntrsumo1  27504  selbergr  27507  iscgrgd  28492  elee  28873  xrge0tsmsd  33040  nn0omnd  33307  xrge0slmod  33311  raddcn  33940  rrhcn  34008  qqtopn  34022  dmvlsiga  34140  ddeval1  34245  ddeval0  34246  ddemeas  34247  mbfmcnt  34279  sxbrsigalem0  34282  sxbrsigalem3  34283  sxbrsigalem2  34297  isrrvv  34454  dstfrvclim1  34489  signsplypnf  34561  erdsze2lem1  35245  erdsze2lem2  35246  snmlval  35373  knoppcnlem5  36537  knoppcnlem6  36538  knoppcnlem7  36539  knoppcnlem8  36540  cnndvlem2  36578  icoreresf  37392  icoreval  37393  poimirlem29  37695  poimirlem30  37696  poimirlem31  37697  poimir  37699  broucube  37700  mblfinlem3  37705  itg2addnclem  37717  itg2addnclem3  37719  itg2addnc  37720  itg2gt0cn  37721  ibladdnclem  37722  itgaddnclem1  37724  iblabsnclem  37729  iblabsnc  37730  iblmulc2nc  37731  itgmulc2nclem1  37732  ftc1anclem3  37741  ftc1anclem4  37742  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  filbcmb  37786  rrncmslem  37878  repwsmet  37880  rrnequiv  37881  ismrer1  37884  absex  42287  pell1qrval  42885  pell14qrval  42887  pell1234qrval  42889  k0004ss1  44190  addrval  44504  subrval  44505  mulvval  44506  rpex  45391  climreeq  45659  limsupre  45685  limcresiooub  45686  limcresioolb  45687  limsuppnfdlem  45745  limsuppnflem  45754  limsupmnflem  45764  limsupre2lem  45768  xlimclim  45868  icccncfext  45931  cncfiooicclem1  45937  itgsubsticclem  46019  ovolsplit  46032  dirkerval  46135  dirkercncflem4  46150  fourierdlem14  46165  fourierdlem15  46166  fourierdlem32  46183  fourierdlem33  46184  fourierdlem54  46204  fourierdlem62  46212  fourierdlem70  46220  fourierdlem81  46231  fourierdlem92  46242  fourierdlem102  46252  fourierdlem111  46261  fourierdlem114  46264  etransclem2  46280  rrxtopn0  46337  qndenserrnbllem  46338  qndenserrnbl  46339  qndenserrn  46343  rrnprjdstle  46345  ioorrnopnlem  46348  dmvolsal  46390  hoicvr  46592  hoissrrn  46593  hoiprodcl2  46599  hoicvrrex  46600  ovn0lem  46609  ovn02  46612  hsphoif  46620  hoidmvval  46621  hoissrrn2  46622  hsphoival  46623  hoidmvlelem3  46641  hoidmvle  46644  ovnhoilem1  46645  ovnhoilem2  46646  ovnhoi  46647  hspval  46653  ovnlecvr2  46654  ovncvr2  46655  hoidifhspval2  46659  hoiqssbl  46669  hspmbllem2  46671  hspmbl  46673  hoimbl  46675  opnvonmbllem2  46677  ovolval2lem  46687  ovolval2  46688  ovolval3  46691  ovolval4lem2  46694  ovolval5lem2  46697  ovnovollem1  46700  ovnovollem2  46701  ovnovollem3  46702  vonvolmbllem  46704  vonvolmbl  46705  vitali2  46738  issmflem  46771  incsmf  46786  decsmf  46811  nsssmfmbflem  46822  smfresal  46832  smfmullem4  46838  smf2id  46845  refdivpm  48582  elbigo2  48590  elbigof  48592  elbigodm  48593  elbigoimp  48594  elbigolo1  48595  prelrrx2  48751  rrx2xpref1o  48756  rrx2xpreen  48757  rrx2linesl  48781  line2  48790  line2x  48792  line2y  48793  amgmlemALT  49841