Theorem reex 11192

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11182	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11158	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5294	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ℂcc 11099  ℝcr 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-cnex 11157  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3913  df-ss 3923

This theorem is referenced by:  reelprrecn  11193  negfi  12165  xrex  13012  limsuple  15531  limsuplt  15532  limsupbnd1  15535  rlim  15548  rlimf  15554  rlimss  15555  ello12  15569  lo1f  15571  lo1dm  15572  elo12  15580  o1f  15582  o1dm  15583  o1of2  15666  o1rlimmul  15672  o1add2  15677  o1mul2  15678  o1sub2  15679  o1dif  15683  caucvgrlem  15726  fsumo1  15866  rpnnen  16284  cpnnen  16286  ruclem13  16299  ruc  16300  aleph1re  16302  aleph1irr  16303  cnfldds  21515  replusg  21741  remulr  21742  rele2  21745  reds  21747  refldcj  21751  ismet  24461  tngngp2  24790  tngngpd  24791  tngngp  24792  tngngp3  24794  nrmtngnrm  24796  tngnrg  24812  rerest  24942  xrtgioo  24945  xrrest  24946  xrsmopn  24951  opnreen  24970  rectbntr0  24971  xrge0tsms  24973  bcthlem1  25464  bcthlem5  25468  reust  25521  rrxip  25530  rrx0el  25538  ehl0base  25556  ehl1eudis  25560  ehl2eudis  25562  pmltpclem2  25589  ovolficcss  25609  ovolval  25613  elovolmlem  25614  ovolctb2  25632  ismbl  25666  mblsplit  25672  voliunlem3  25692  dyadmbl  25740  vitalilem2  25749  vitalilem3  25750  vitalilem4  25751  vitalilem5  25752  vitali  25753  mbff  25765  ismbf  25768  ismbfcn  25769  mbfconst  25773  cncombf  25798  cnmbf  25799  0plef  25812  i1fd  25821  itg1ge0  25826  i1faddlem  25833  i1fmullem  25834  i1fadd  25835  i1fmul  25836  itg1addlem4  25839  i1fmulclem  25842  i1fmulc  25843  itg1mulc  25844  i1fsub  25848  itg1sub  25849  itg1lea  25852  itg1le  25853  mbfi1fseqlem2  25856  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1flimlem  25862  mbfmullem2  25864  itg2val  25868  xrge0f  25871  itg2ge0  25875  itg2itg1  25876  itg20  25877  itg2le  25879  itg2const  25880  itg2const2  25881  itg2seq  25882  itg2uba  25883  itg2lea  25884  itg2mulclem  25886  itg2mulc  25887  itg2splitlem  25888  itg2split  25889  itg2monolem1  25890  itg2mono  25893  itg2i1fseqle  25894  itg2i1fseq  25895  itg2addlem  25898  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  iblss  25945  i1fibl  25948  itgitg1  25949  itgle  25950  ibladdlem  25960  itgaddlem1  25963  iblabslem  25968  iblabs  25969  iblabsr  25970  iblmulc2  25971  itgmulc2lem1  25972  bddmulibl  25979  bddiblnc  25982  dvnfre  26092  c1liplem1  26136  c1lip2  26138  lhop2  26155  dvcnvrelem2  26158  taylthlem2  26518  dmarea  27103  vmadivsum  27627  rpvmasumlem  27632  mudivsum  27675  selberglem1  27690  selberglem2  27691  selberg2lem  27695  selberg2  27696  pntrsumo1  27710  selbergr  27713  iscgrgd  28763  elee  29224  xrge0tsmsd  33374  nn0omnd  33645  xrge0slmod  33649  raddcn  34300  rrhcn  34368  qqtopn  34382  dmvlsiga  34500  ddeval1  34605  ddeval0  34606  ddemeas  34607  mbfmcnt  34639  sxbrsigalem0  34642  sxbrsigalem3  34643  sxbrsigalem2  34657  isrrvv  34814  dstfrvclim1  34849  signsplypnf  34918  erdsze2lem1  35676  erdsze2lem2  35677  snmlval  35804  knoppcnlem5  37067  knoppcnlem6  37068  knoppcnlem7  37069  knoppcnlem8  37070  cnndvlem2  37108  icoreresf  37979  icoreval  37980  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  poimir  38285  broucube  38286  mblfinlem3  38291  itg2addnclem  38303  itg2addnclem3  38305  itg2addnc  38306  itg2gt0cn  38307  ibladdnclem  38308  itgaddnclem1  38310  iblabsnclem  38315  iblabsnc  38316  iblmulc2nc  38317  itgmulc2nclem1  38318  ftc1anclem3  38327  ftc1anclem4  38328  ftc1anclem5  38329  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  filbcmb  38372  rrncmslem  38464  repwsmet  38466  rrnequiv  38467  ismrer1  38470  absex  42997  pell1qrval  43556  pell14qrval  43558  pell1234qrval  43560  k0004ss1  44860  addrval  45157  subrval  45158  mulvval  45159  rpex  46045  climreeq  46312  limsupre  46338  limcresiooub  46339  limcresioolb  46340  limsuppnfdlem  46398  limsuppnflem  46407  limsupmnflem  46417  limsupre2lem  46421  xlimclim  46521  icccncfext  46584  cncfiooicclem1  46590  itgsubsticclem  46672  ovolsplit  46685  dirkerval  46788  dirkercncflem4  46803  fourierdlem14  46818  fourierdlem15  46819  fourierdlem32  46836  fourierdlem33  46837  fourierdlem54  46857  fourierdlem62  46865  fourierdlem70  46873  fourierdlem81  46884  fourierdlem92  46895  fourierdlem102  46905  fourierdlem111  46914  fourierdlem114  46917  etransclem2  46933  rrxtopn0  46990  qndenserrnbllem  46991  qndenserrnbl  46992  qndenserrn  46996  rrnprjdstle  46998  ioorrnopnlem  47001  dmvolsal  47043  hoicvr  47245  hoissrrn  47246  hoiprodcl2  47252  hoicvrrex  47253  ovn0lem  47262  ovn02  47265  hsphoif  47273  hoidmvval  47274  hoissrrn2  47275  hsphoival  47276  hoidmvlelem3  47294  hoidmvle  47297  ovnhoilem1  47298  ovnhoilem2  47299  ovnhoi  47300  hspval  47306  ovnlecvr2  47307  ovncvr2  47308  hoidifhspval2  47312  hoiqssbl  47322  hspmbllem2  47324  hspmbl  47326  hoimbl  47328  opnvonmbllem2  47330  ovolval2lem  47340  ovolval2  47341  ovolval3  47344  ovolval4lem2  47347  ovolval5lem2  47350  ovnovollem1  47353  ovnovollem2  47354  ovnovollem3  47355  vonvolmbllem  47357  vonvolmbl  47358  vitali2  47391  issmflem  47424  incsmf  47439  decsmf  47464  nsssmfmbflem  47475  smfresal  47485  smfmullem4  47491  smf2id  47498  nthrucw  47590  refdivpm  49307  elbigo2  49315  elbigof  49317  elbigodm  49318  elbigoimp  49319  elbigolo1  49320  prelrrx2  49476  rrx2xpref1o  49481  rrx2xpreen  49482  rrx2linesl  49506  line2  49515  line2x  49517  line2y  49518  amgmlemALT  50586