Theorem reex 11166

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11156	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11132	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5280	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073  ℝcr 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  reelprrecn  11167  negfi  12139  xrex  12953  limsuple  15451  limsuplt  15452  limsupbnd1  15455  rlim  15468  rlimf  15474  rlimss  15475  ello12  15489  lo1f  15491  lo1dm  15492  elo12  15500  o1f  15502  o1dm  15503  o1of2  15586  o1rlimmul  15592  o1add2  15597  o1mul2  15598  o1sub2  15599  o1dif  15603  caucvgrlem  15646  fsumo1  15785  rpnnen  16202  cpnnen  16204  ruclem13  16217  ruc  16218  aleph1re  16220  aleph1irr  16221  cnfldds  21283  cnflddsOLD  21296  replusg  21526  remulr  21527  rele2  21530  reds  21532  refldcj  21536  ismet  24218  tngngp2  24547  tngngpd  24548  tngngp  24549  tngngp3  24551  nrmtngnrm  24553  tngnrg  24569  rerest  24699  xrtgioo  24702  xrrest  24703  xrsmopn  24708  opnreen  24727  rectbntr0  24728  xrge0tsms  24730  bcthlem1  25231  bcthlem5  25235  reust  25288  rrxip  25297  rrx0el  25305  ehl0base  25323  ehl1eudis  25327  ehl2eudis  25329  pmltpclem2  25357  ovolficcss  25377  ovolval  25381  elovolmlem  25382  ovolctb2  25400  ismbl  25434  mblsplit  25440  voliunlem3  25460  dyadmbl  25508  vitalilem2  25517  vitalilem3  25518  vitalilem4  25519  vitalilem5  25520  vitali  25521  mbff  25533  ismbf  25536  ismbfcn  25537  mbfconst  25541  cncombf  25566  cnmbf  25567  0plef  25580  i1fd  25589  itg1ge0  25594  i1faddlem  25601  i1fmullem  25602  i1fadd  25603  i1fmul  25604  itg1addlem4  25607  i1fmulclem  25610  i1fmulc  25611  itg1mulc  25612  i1fsub  25616  itg1sub  25617  itg1lea  25620  itg1le  25621  mbfi1fseqlem2  25624  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1flimlem  25630  mbfmullem2  25632  itg2val  25636  xrge0f  25639  itg2ge0  25643  itg2itg1  25644  itg20  25645  itg2le  25647  itg2const  25648  itg2const2  25649  itg2seq  25650  itg2uba  25651  itg2lea  25652  itg2mulclem  25654  itg2mulc  25655  itg2splitlem  25656  itg2split  25657  itg2monolem1  25658  itg2mono  25661  itg2i1fseqle  25662  itg2i1fseq  25663  itg2addlem  25666  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  i1fibl  25716  itgitg1  25717  itgle  25718  ibladdlem  25728  itgaddlem1  25731  iblabslem  25736  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgmulc2lem1  25740  bddmulibl  25747  bddiblnc  25750  dvnfre  25863  c1liplem1  25908  c1lip2  25910  lhop2  25927  dvcnvrelem2  25930  taylthlem2  26289  taylthlem2OLD  26290  dmarea  26874  vmadivsum  27400  rpvmasumlem  27405  mudivsum  27448  selberglem1  27463  selberglem2  27464  selberg2lem  27468  selberg2  27469  pntrsumo1  27483  selbergr  27486  iscgrgd  28447  elee  28828  xrge0tsmsd  33009  nn0omnd  33323  xrge0slmod  33326  raddcn  33926  rrhcn  33994  qqtopn  34008  dmvlsiga  34126  ddeval1  34231  ddeval0  34232  ddemeas  34233  mbfmcnt  34266  sxbrsigalem0  34269  sxbrsigalem3  34270  sxbrsigalem2  34284  isrrvv  34441  dstfrvclim1  34476  signsplypnf  34548  erdsze2lem1  35197  erdsze2lem2  35198  snmlval  35325  knoppcnlem5  36492  knoppcnlem6  36493  knoppcnlem7  36494  knoppcnlem8  36495  cnndvlem2  36533  icoreresf  37347  icoreval  37348  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimir  37654  broucube  37655  mblfinlem3  37660  itg2addnclem  37672  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem1  37679  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  itgmulc2nclem1  37687  ftc1anclem3  37696  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  filbcmb  37741  rrncmslem  37833  repwsmet  37835  rrnequiv  37836  ismrer1  37839  absex  42243  pell1qrval  42841  pell14qrval  42843  pell1234qrval  42845  k0004ss1  44147  addrval  44462  subrval  44463  mulvval  44464  rpex  45349  climreeq  45618  limsupre  45646  limcresiooub  45647  limcresioolb  45648  limsuppnfdlem  45706  limsuppnflem  45715  limsupmnflem  45725  limsupre2lem  45729  xlimclim  45829  icccncfext  45892  cncfiooicclem1  45898  itgsubsticclem  45980  ovolsplit  45993  dirkerval  46096  dirkercncflem4  46111  fourierdlem14  46126  fourierdlem15  46127  fourierdlem32  46144  fourierdlem33  46145  fourierdlem54  46165  fourierdlem62  46173  fourierdlem70  46181  fourierdlem81  46192  fourierdlem92  46203  fourierdlem102  46213  fourierdlem111  46222  fourierdlem114  46225  etransclem2  46241  rrxtopn0  46298  qndenserrnbllem  46299  qndenserrnbl  46300  qndenserrn  46304  rrnprjdstle  46306  ioorrnopnlem  46309  dmvolsal  46351  hoicvr  46553  hoissrrn  46554  hoiprodcl2  46560  hoicvrrex  46561  ovn0lem  46570  ovn02  46573  hsphoif  46581  hoidmvval  46582  hoissrrn2  46583  hsphoival  46584  hoidmvlelem3  46602  hoidmvle  46605  ovnhoilem1  46606  ovnhoilem2  46607  ovnhoi  46608  hspval  46614  ovnlecvr2  46615  ovncvr2  46616  hoidifhspval2  46620  hoiqssbl  46630  hspmbllem2  46632  hspmbl  46634  hoimbl  46636  opnvonmbllem2  46638  ovolval2lem  46648  ovolval2  46649  ovolval3  46652  ovolval4lem2  46655  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  ovnovollem3  46663  vonvolmbllem  46665  vonvolmbl  46666  vitali2  46699  issmflem  46732  incsmf  46747  decsmf  46772  nsssmfmbflem  46783  smfresal  46793  smfmullem4  46799  smf2id  46806  refdivpm  48537  elbigo2  48545  elbigof  48547  elbigodm  48548  elbigoimp  48549  elbigolo1  48550  prelrrx2  48706  rrx2xpref1o  48711  rrx2xpreen  48712  rrx2linesl  48736  line2  48745  line2x  48747  line2y  48748  amgmlemALT  49796