Theorem reex 11246

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11236	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11212	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5322	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ℂcc 11153  ℝcr 11154

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  reelprrecn  11247  negfi  12217  xrex  13029  limsuple  15514  limsuplt  15515  limsupbnd1  15518  rlim  15531  rlimf  15537  rlimss  15538  ello12  15552  lo1f  15554  lo1dm  15555  elo12  15563  o1f  15565  o1dm  15566  o1of2  15649  o1rlimmul  15655  o1add2  15660  o1mul2  15661  o1sub2  15662  o1dif  15666  caucvgrlem  15709  fsumo1  15848  rpnnen  16263  cpnnen  16265  ruclem13  16278  ruc  16279  aleph1re  16281  aleph1irr  16282  cnfldds  21376  cnflddsOLD  21389  replusg  21628  remulr  21629  rele2  21632  reds  21634  refldcj  21638  ismet  24333  tngngp2  24673  tngngpd  24674  tngngp  24675  tngngp3  24677  nrmtngnrm  24679  tngnrg  24695  rerest  24825  xrtgioo  24828  xrrest  24829  xrsmopn  24834  opnreen  24853  rectbntr0  24854  xrge0tsms  24856  bcthlem1  25358  bcthlem5  25362  reust  25415  rrxip  25424  rrx0el  25432  ehl0base  25450  ehl1eudis  25454  ehl2eudis  25456  pmltpclem2  25484  ovolficcss  25504  ovolval  25508  elovolmlem  25509  ovolctb2  25527  ismbl  25561  mblsplit  25567  voliunlem3  25587  dyadmbl  25635  vitalilem2  25644  vitalilem3  25645  vitalilem4  25646  vitalilem5  25647  vitali  25648  mbff  25660  ismbf  25663  ismbfcn  25664  mbfconst  25668  cncombf  25693  cnmbf  25694  0plef  25707  i1fd  25716  itg1ge0  25721  i1faddlem  25728  i1fmullem  25729  i1fadd  25730  i1fmul  25731  itg1addlem4  25734  i1fmulclem  25737  i1fmulc  25738  itg1mulc  25739  i1fsub  25743  itg1sub  25744  itg1lea  25747  itg1le  25748  mbfi1fseqlem2  25751  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1flimlem  25757  mbfmullem2  25759  itg2val  25763  xrge0f  25766  itg2ge0  25770  itg2itg1  25771  itg20  25772  itg2le  25774  itg2const  25775  itg2const2  25776  itg2seq  25777  itg2uba  25778  itg2lea  25779  itg2mulclem  25781  itg2mulc  25782  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  i1fibl  25843  itgitg1  25844  itgle  25845  ibladdlem  25855  itgaddlem1  25858  iblabslem  25863  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgmulc2lem1  25867  bddmulibl  25874  bddiblnc  25877  dvnfre  25990  c1liplem1  26035  c1lip2  26037  lhop2  26054  dvcnvrelem2  26057  taylthlem2  26416  taylthlem2OLD  26417  dmarea  27000  vmadivsum  27526  rpvmasumlem  27531  mudivsum  27574  selberglem1  27589  selberglem2  27590  selberg2lem  27594  selberg2  27595  pntrsumo1  27609  selbergr  27612  iscgrgd  28521  elee  28909  xrge0tsmsd  33065  nn0omnd  33373  xrge0slmod  33376  raddcn  33928  rrhcn  33998  qqtopn  34012  dmvlsiga  34130  ddeval1  34235  ddeval0  34236  ddemeas  34237  mbfmcnt  34270  sxbrsigalem0  34273  sxbrsigalem3  34274  sxbrsigalem2  34288  isrrvv  34445  dstfrvclim1  34480  signsplypnf  34565  erdsze2lem1  35208  erdsze2lem2  35209  snmlval  35336  knoppcnlem5  36498  knoppcnlem6  36499  knoppcnlem7  36500  knoppcnlem8  36501  cnndvlem2  36539  icoreresf  37353  icoreval  37354  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimir  37660  broucube  37661  mblfinlem3  37666  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem1  37685  iblabsnclem  37690  iblabsnc  37691  iblmulc2nc  37692  itgmulc2nclem1  37693  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  filbcmb  37747  rrncmslem  37839  repwsmet  37841  rrnequiv  37842  ismrer1  37845  absex  42289  pell1qrval  42857  pell14qrval  42859  pell1234qrval  42861  k0004ss1  44164  addrval  44485  subrval  44486  mulvval  44487  rpex  45357  climreeq  45628  limsupre  45656  limcresiooub  45657  limcresioolb  45658  limsuppnfdlem  45716  limsuppnflem  45725  limsupmnflem  45735  limsupre2lem  45739  xlimclim  45839  icccncfext  45902  cncfiooicclem1  45908  itgsubsticclem  45990  ovolsplit  46003  dirkerval  46106  dirkercncflem4  46121  fourierdlem14  46136  fourierdlem15  46137  fourierdlem32  46154  fourierdlem33  46155  fourierdlem54  46175  fourierdlem62  46183  fourierdlem70  46191  fourierdlem81  46202  fourierdlem92  46213  fourierdlem102  46223  fourierdlem111  46232  fourierdlem114  46235  etransclem2  46251  rrxtopn0  46308  qndenserrnbllem  46309  qndenserrnbl  46310  qndenserrn  46314  rrnprjdstle  46316  ioorrnopnlem  46319  dmvolsal  46361  hoicvr  46563  hoissrrn  46564  hoiprodcl2  46570  hoicvrrex  46571  ovn0lem  46580  ovn02  46583  hsphoif  46591  hoidmvval  46592  hoissrrn2  46593  hsphoival  46594  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem1  46616  ovnhoilem2  46617  ovnhoi  46618  hspval  46624  ovnlecvr2  46625  ovncvr2  46626  hoidifhspval2  46630  hoiqssbl  46640  hspmbllem2  46642  hspmbl  46644  hoimbl  46646  opnvonmbllem2  46648  ovolval2lem  46658  ovolval2  46659  ovolval3  46662  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  ovnovollem3  46673  vonvolmbllem  46675  vonvolmbl  46676  vitali2  46709  issmflem  46742  incsmf  46757  decsmf  46782  nsssmfmbflem  46793  smfresal  46803  smfmullem4  46809  smf2id  46816  refdivpm  48465  elbigo2  48473  elbigof  48475  elbigodm  48476  elbigoimp  48477  elbigolo1  48478  prelrrx2  48634  rrx2xpref1o  48639  rrx2xpreen  48640  rrx2linesl  48664  line2  48673  line2x  48675  line2y  48676  amgmlemALT  49322