Theorem reex 11198

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ℂcc 11105  ℝcr 11106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-cnex 11163  ax-resscn 11164

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  reelprrecn  11199  negfi  12160  xrex  12968  limsuple  15419  limsuplt  15420  limsupbnd1  15423  rlim  15436  rlimf  15442  rlimss  15443  ello12  15457  lo1f  15459  lo1dm  15460  elo12  15468  o1f  15470  o1dm  15471  o1of2  15554  o1rlimmul  15560  o1add2  15565  o1mul2  15566  o1sub2  15567  o1dif  15571  caucvgrlem  15616  fsumo1  15755  rpnnen  16167  cpnnen  16169  ruclem13  16182  ruc  16183  aleph1re  16185  aleph1irr  16186  cnfldds  20947  replusg  21155  remulr  21156  rele2  21159  reds  21161  refldcj  21165  ismet  23821  tngngp2  24161  tngngpd  24162  tngngp  24163  tngngp3  24165  nrmtngnrm  24167  tngnrg  24183  rerest  24312  xrtgioo  24314  xrrest  24315  xrsmopn  24320  opnreen  24339  rectbntr0  24340  xrge0tsms  24342  bcthlem1  24833  bcthlem5  24837  reust  24890  rrxip  24899  rrx0el  24907  ehl0base  24925  ehl1eudis  24929  ehl2eudis  24931  pmltpclem2  24958  ovolficcss  24978  ovolval  24982  elovolmlem  24983  ovolctb2  25001  ismbl  25035  mblsplit  25041  voliunlem3  25061  dyadmbl  25109  vitalilem2  25118  vitalilem3  25119  vitalilem4  25120  vitalilem5  25121  vitali  25122  mbff  25134  ismbf  25137  ismbfcn  25138  mbfconst  25142  cncombf  25167  cnmbf  25168  0plef  25181  i1fd  25190  itg1ge0  25195  i1faddlem  25202  i1fmullem  25203  i1fadd  25204  i1fmul  25205  itg1addlem4  25208  itg1addlem4OLD  25209  i1fmulclem  25212  i1fmulc  25213  itg1mulc  25214  i1fsub  25218  itg1sub  25219  itg1lea  25222  itg1le  25223  mbfi1fseqlem2  25226  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1flimlem  25232  mbfmullem2  25234  itg2val  25238  xrge0f  25241  itg2ge0  25245  itg2itg1  25246  itg20  25247  itg2le  25249  itg2const  25250  itg2const2  25251  itg2seq  25252  itg2uba  25253  itg2lea  25254  itg2mulclem  25256  itg2mulc  25257  itg2splitlem  25258  itg2split  25259  itg2monolem1  25260  itg2mono  25263  itg2i1fseqle  25264  itg2i1fseq  25265  itg2addlem  25268  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  iblss  25314  i1fibl  25317  itgitg1  25318  itgle  25319  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgmulc2lem1  25341  bddmulibl  25348  bddiblnc  25351  dvnfre  25461  c1liplem1  25505  c1lip2  25507  lhop2  25524  dvcnvrelem2  25527  taylthlem2  25878  dmarea  26452  vmadivsum  26975  rpvmasumlem  26980  mudivsum  27023  selberglem1  27038  selberglem2  27039  selberg2lem  27043  selberg2  27044  pntrsumo1  27058  selbergr  27061  iscgrgd  27754  elee  28142  xrge0tsmsd  32197  nn0omnd  32449  xrge0slmod  32452  raddcn  32898  rrhcn  32966  qqtopn  32980  dmvlsiga  33116  ddeval1  33221  ddeval0  33222  ddemeas  33223  mbfmcnt  33256  sxbrsigalem0  33259  sxbrsigalem3  33260  sxbrsigalem2  33274  isrrvv  33431  dstfrvclim1  33465  signsplypnf  33550  erdsze2lem1  34183  erdsze2lem2  34184  snmlval  34311  knoppcnlem5  35362  knoppcnlem6  35363  knoppcnlem7  35364  knoppcnlem8  35365  cnndvlem2  35403  icoreresf  36222  icoreval  36223  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimir  36510  broucube  36511  mblfinlem3  36516  itg2addnclem  36528  itg2addnclem3  36530  itg2addnc  36531  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nclem1  36543  ftc1anclem3  36552  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  filbcmb  36597  rrncmslem  36689  repwsmet  36691  rrnequiv  36692  ismrer1  36695  pell1qrval  41570  pell14qrval  41572  pell1234qrval  41574  k0004ss1  42888  addrval  43211  subrval  43212  mulvval  43213  climreeq  44316  limsupre  44344  limcresiooub  44345  limcresioolb  44346  limsuppnfdlem  44404  limsuppnflem  44413  limsupmnflem  44423  limsupre2lem  44427  xlimclim  44527  icccncfext  44590  cncfiooicclem1  44596  itgsubsticclem  44678  ovolsplit  44691  dirkerval  44794  dirkercncflem4  44809  fourierdlem14  44824  fourierdlem15  44825  fourierdlem32  44842  fourierdlem33  44843  fourierdlem54  44863  fourierdlem62  44871  fourierdlem70  44879  fourierdlem81  44890  fourierdlem92  44901  fourierdlem102  44911  fourierdlem111  44920  fourierdlem114  44923  etransclem2  44939  rrxtopn0  44996  qndenserrnbllem  44997  qndenserrnbl  44998  qndenserrn  45002  rrnprjdstle  45004  ioorrnopnlem  45007  dmvolsal  45049  hoicvr  45251  hoissrrn  45252  hoiprodcl2  45258  hoicvrrex  45259  ovn0lem  45268  ovn02  45271  hsphoif  45279  hoidmvval  45280  hoissrrn2  45281  hsphoival  45282  hoidmvlelem3  45300  hoidmvle  45303  ovnhoilem1  45304  ovnhoilem2  45305  ovnhoi  45306  hspval  45312  ovnlecvr2  45313  ovncvr2  45314  hoidifhspval2  45318  hoiqssbl  45328  hspmbllem2  45330  hspmbl  45332  hoimbl  45334  opnvonmbllem2  45336  ovolval2lem  45346  ovolval2  45347  ovolval3  45350  ovolval4lem2  45353  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  ovnovollem3  45361  vonvolmbllem  45363  vonvolmbl  45364  vitali2  45397  issmflem  45430  incsmf  45445  decsmf  45470  nsssmfmbflem  45481  smfresal  45491  smfmullem4  45497  smf2id  45504  refdivpm  47184  elbigo2  47192  elbigof  47194  elbigodm  47195  elbigoimp  47196  elbigolo1  47197  prelrrx2  47353  rrx2xpref1o  47358  rrx2xpreen  47359  rrx2linesl  47383  line2  47392  line2x  47394  line2y  47395  amgmlemALT  47804