Theorem reex 11108

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11098	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11074	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5264	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ℂcc 11015  ℝcr 11016

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-cnex 11073  ax-resscn 11074

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915

This theorem is referenced by:  reelprrecn  11109  negfi  12082  xrex  12891  limsuple  15392  limsuplt  15393  limsupbnd1  15396  rlim  15409  rlimf  15415  rlimss  15416  ello12  15430  lo1f  15432  lo1dm  15433  elo12  15441  o1f  15443  o1dm  15444  o1of2  15527  o1rlimmul  15533  o1add2  15538  o1mul2  15539  o1sub2  15540  o1dif  15544  caucvgrlem  15587  fsumo1  15726  rpnnen  16143  cpnnen  16145  ruclem13  16158  ruc  16159  aleph1re  16161  aleph1irr  16162  cnfldds  21312  cnflddsOLD  21325  replusg  21556  remulr  21557  rele2  21560  reds  21562  refldcj  21566  ismet  24258  tngngp2  24587  tngngpd  24588  tngngp  24589  tngngp3  24591  nrmtngnrm  24593  tngnrg  24609  rerest  24739  xrtgioo  24742  xrrest  24743  xrsmopn  24748  opnreen  24767  rectbntr0  24768  xrge0tsms  24770  bcthlem1  25271  bcthlem5  25275  reust  25328  rrxip  25337  rrx0el  25345  ehl0base  25363  ehl1eudis  25367  ehl2eudis  25369  pmltpclem2  25397  ovolficcss  25417  ovolval  25421  elovolmlem  25422  ovolctb2  25440  ismbl  25474  mblsplit  25480  voliunlem3  25500  dyadmbl  25548  vitalilem2  25557  vitalilem3  25558  vitalilem4  25559  vitalilem5  25560  vitali  25561  mbff  25573  ismbf  25576  ismbfcn  25577  mbfconst  25581  cncombf  25606  cnmbf  25607  0plef  25620  i1fd  25629  itg1ge0  25634  i1faddlem  25641  i1fmullem  25642  i1fadd  25643  i1fmul  25644  itg1addlem4  25647  i1fmulclem  25650  i1fmulc  25651  itg1mulc  25652  i1fsub  25656  itg1sub  25657  itg1lea  25660  itg1le  25661  mbfi1fseqlem2  25664  mbfi1fseqlem4  25666  mbfi1fseqlem5  25667  mbfi1flimlem  25670  mbfmullem2  25672  itg2val  25676  xrge0f  25679  itg2ge0  25683  itg2itg1  25684  itg20  25685  itg2le  25687  itg2const  25688  itg2const2  25689  itg2seq  25690  itg2uba  25691  itg2lea  25692  itg2mulclem  25694  itg2mulc  25695  itg2splitlem  25696  itg2split  25697  itg2monolem1  25698  itg2mono  25701  itg2i1fseqle  25702  itg2i1fseq  25703  itg2addlem  25706  itg2gt0  25708  itg2cnlem1  25709  itg2cnlem2  25710  iblss  25753  i1fibl  25756  itgitg1  25757  itgle  25758  ibladdlem  25768  itgaddlem1  25771  iblabslem  25776  iblabs  25777  iblabsr  25778  iblmulc2  25779  itgmulc2lem1  25780  bddmulibl  25787  bddiblnc  25790  dvnfre  25903  c1liplem1  25948  c1lip2  25950  lhop2  25967  dvcnvrelem2  25970  taylthlem2  26329  taylthlem2OLD  26330  dmarea  26914  vmadivsum  27440  rpvmasumlem  27445  mudivsum  27488  selberglem1  27503  selberglem2  27504  selberg2lem  27508  selberg2  27509  pntrsumo1  27523  selbergr  27526  iscgrgd  28511  elee  28892  xrge0tsmsd  33083  nn0omnd  33353  xrge0slmod  33357  raddcn  34014  rrhcn  34082  qqtopn  34096  dmvlsiga  34214  ddeval1  34319  ddeval0  34320  ddemeas  34321  mbfmcnt  34353  sxbrsigalem0  34356  sxbrsigalem3  34357  sxbrsigalem2  34371  isrrvv  34528  dstfrvclim1  34563  signsplypnf  34635  erdsze2lem1  35319  erdsze2lem2  35320  snmlval  35447  knoppcnlem5  36613  knoppcnlem6  36614  knoppcnlem7  36615  knoppcnlem8  36616  cnndvlem2  36654  icoreresf  37469  icoreval  37470  poimirlem29  37762  poimirlem30  37763  poimirlem31  37764  poimir  37766  broucube  37767  mblfinlem3  37772  itg2addnclem  37784  itg2addnclem3  37786  itg2addnc  37787  itg2gt0cn  37788  ibladdnclem  37789  itgaddnclem1  37791  iblabsnclem  37796  iblabsnc  37797  iblmulc2nc  37798  itgmulc2nclem1  37799  ftc1anclem3  37808  ftc1anclem4  37809  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  filbcmb  37853  rrncmslem  37945  repwsmet  37947  rrnequiv  37948  ismrer1  37951  absex  42418  pell1qrval  43003  pell14qrval  43005  pell1234qrval  43007  k0004ss1  44308  addrval  44622  subrval  44623  mulvval  44624  rpex  45507  climreeq  45775  limsupre  45801  limcresiooub  45802  limcresioolb  45803  limsuppnfdlem  45861  limsuppnflem  45870  limsupmnflem  45880  limsupre2lem  45884  xlimclim  45984  icccncfext  46047  cncfiooicclem1  46053  itgsubsticclem  46135  ovolsplit  46148  dirkerval  46251  dirkercncflem4  46266  fourierdlem14  46281  fourierdlem15  46282  fourierdlem32  46299  fourierdlem33  46300  fourierdlem54  46320  fourierdlem62  46328  fourierdlem70  46336  fourierdlem81  46347  fourierdlem92  46358  fourierdlem102  46368  fourierdlem111  46377  fourierdlem114  46380  etransclem2  46396  rrxtopn0  46453  qndenserrnbllem  46454  qndenserrnbl  46455  qndenserrn  46459  rrnprjdstle  46461  ioorrnopnlem  46464  dmvolsal  46506  hoicvr  46708  hoissrrn  46709  hoiprodcl2  46715  hoicvrrex  46716  ovn0lem  46725  ovn02  46728  hsphoif  46736  hoidmvval  46737  hoissrrn2  46738  hsphoival  46739  hoidmvlelem3  46757  hoidmvle  46760  ovnhoilem1  46761  ovnhoilem2  46762  ovnhoi  46763  hspval  46769  ovnlecvr2  46770  ovncvr2  46771  hoidifhspval2  46775  hoiqssbl  46785  hspmbllem2  46787  hspmbl  46789  hoimbl  46791  opnvonmbllem2  46793  ovolval2lem  46803  ovolval2  46804  ovolval3  46807  ovolval4lem2  46810  ovolval5lem2  46813  ovnovollem1  46816  ovnovollem2  46817  ovnovollem3  46818  vonvolmbllem  46820  vonvolmbl  46821  vitali2  46854  issmflem  46887  incsmf  46902  decsmf  46927  nsssmfmbflem  46938  smfresal  46948  smfmullem4  46954  smf2id  46961  nthrucw  47046  refdivpm  48706  elbigo2  48714  elbigof  48716  elbigodm  48717  elbigoimp  48718  elbigolo1  48719  prelrrx2  48875  rrx2xpref1o  48880  rrx2xpreen  48881  rrx2linesl  48905  line2  48914  line2x  48916  line2y  48917  amgmlemALT  49964