Theorem reex 11218

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11208	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11184	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5292	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ℂcc 11125  ℝcr 11126

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 2707  ax-sep 5266  ax-cnex 11183  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  reelprrecn  11219  negfi  12189  xrex  13001  limsuple  15492  limsuplt  15493  limsupbnd1  15496  rlim  15509  rlimf  15515  rlimss  15516  ello12  15530  lo1f  15532  lo1dm  15533  elo12  15541  o1f  15543  o1dm  15544  o1of2  15627  o1rlimmul  15633  o1add2  15638  o1mul2  15639  o1sub2  15640  o1dif  15644  caucvgrlem  15687  fsumo1  15826  rpnnen  16243  cpnnen  16245  ruclem13  16258  ruc  16259  aleph1re  16261  aleph1irr  16262  cnfldds  21325  cnflddsOLD  21338  replusg  21568  remulr  21569  rele2  21572  reds  21574  refldcj  21578  ismet  24260  tngngp2  24589  tngngpd  24590  tngngp  24591  tngngp3  24593  nrmtngnrm  24595  tngnrg  24611  rerest  24741  xrtgioo  24744  xrrest  24745  xrsmopn  24750  opnreen  24769  rectbntr0  24770  xrge0tsms  24772  bcthlem1  25274  bcthlem5  25278  reust  25331  rrxip  25340  rrx0el  25348  ehl0base  25366  ehl1eudis  25370  ehl2eudis  25372  pmltpclem2  25400  ovolficcss  25420  ovolval  25424  elovolmlem  25425  ovolctb2  25443  ismbl  25477  mblsplit  25483  voliunlem3  25503  dyadmbl  25551  vitalilem2  25560  vitalilem3  25561  vitalilem4  25562  vitalilem5  25563  vitali  25564  mbff  25576  ismbf  25579  ismbfcn  25580  mbfconst  25584  cncombf  25609  cnmbf  25610  0plef  25623  i1fd  25632  itg1ge0  25637  i1faddlem  25644  i1fmullem  25645  i1fadd  25646  i1fmul  25647  itg1addlem4  25650  i1fmulclem  25653  i1fmulc  25654  itg1mulc  25655  i1fsub  25659  itg1sub  25660  itg1lea  25663  itg1le  25664  mbfi1fseqlem2  25667  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1flimlem  25673  mbfmullem2  25675  itg2val  25679  xrge0f  25682  itg2ge0  25686  itg2itg1  25687  itg20  25688  itg2le  25690  itg2const  25691  itg2const2  25692  itg2seq  25693  itg2uba  25694  itg2lea  25695  itg2mulclem  25697  itg2mulc  25698  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2mono  25704  itg2i1fseqle  25705  itg2i1fseq  25706  itg2addlem  25709  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  iblss  25756  i1fibl  25759  itgitg1  25760  itgle  25761  ibladdlem  25771  itgaddlem1  25774  iblabslem  25779  iblabs  25780  iblabsr  25781  iblmulc2  25782  itgmulc2lem1  25783  bddmulibl  25790  bddiblnc  25793  dvnfre  25906  c1liplem1  25951  c1lip2  25953  lhop2  25970  dvcnvrelem2  25973  taylthlem2  26332  taylthlem2OLD  26333  dmarea  26917  vmadivsum  27443  rpvmasumlem  27448  mudivsum  27491  selberglem1  27506  selberglem2  27507  selberg2lem  27511  selberg2  27512  pntrsumo1  27526  selbergr  27529  iscgrgd  28438  elee  28819  xrge0tsmsd  33002  nn0omnd  33306  xrge0slmod  33309  raddcn  33906  rrhcn  33974  qqtopn  33988  dmvlsiga  34106  ddeval1  34211  ddeval0  34212  ddemeas  34213  mbfmcnt  34246  sxbrsigalem0  34249  sxbrsigalem3  34250  sxbrsigalem2  34264  isrrvv  34421  dstfrvclim1  34456  signsplypnf  34528  erdsze2lem1  35171  erdsze2lem2  35172  snmlval  35299  knoppcnlem5  36461  knoppcnlem6  36462  knoppcnlem7  36463  knoppcnlem8  36464  cnndvlem2  36502  icoreresf  37316  icoreval  37317  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimir  37623  broucube  37624  mblfinlem3  37629  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ibladdnclem  37646  itgaddnclem1  37648  iblabsnclem  37653  iblabsnc  37654  iblmulc2nc  37655  itgmulc2nclem1  37656  ftc1anclem3  37665  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  filbcmb  37710  rrncmslem  37802  repwsmet  37804  rrnequiv  37805  ismrer1  37808  absex  42246  pell1qrval  42816  pell14qrval  42818  pell1234qrval  42820  k0004ss1  44122  addrval  44438  subrval  44439  mulvval  44440  rpex  45321  climreeq  45590  limsupre  45618  limcresiooub  45619  limcresioolb  45620  limsuppnfdlem  45678  limsuppnflem  45687  limsupmnflem  45697  limsupre2lem  45701  xlimclim  45801  icccncfext  45864  cncfiooicclem1  45870  itgsubsticclem  45952  ovolsplit  45965  dirkerval  46068  dirkercncflem4  46083  fourierdlem14  46098  fourierdlem15  46099  fourierdlem32  46116  fourierdlem33  46117  fourierdlem54  46137  fourierdlem62  46145  fourierdlem70  46153  fourierdlem81  46164  fourierdlem92  46175  fourierdlem102  46185  fourierdlem111  46194  fourierdlem114  46197  etransclem2  46213  rrxtopn0  46270  qndenserrnbllem  46271  qndenserrnbl  46272  qndenserrn  46276  rrnprjdstle  46278  ioorrnopnlem  46281  dmvolsal  46323  hoicvr  46525  hoissrrn  46526  hoiprodcl2  46532  hoicvrrex  46533  ovn0lem  46542  ovn02  46545  hsphoif  46553  hoidmvval  46554  hoissrrn2  46555  hsphoival  46556  hoidmvlelem3  46574  hoidmvle  46577  ovnhoilem1  46578  ovnhoilem2  46579  ovnhoi  46580  hspval  46586  ovnlecvr2  46587  ovncvr2  46588  hoidifhspval2  46592  hoiqssbl  46602  hspmbllem2  46604  hspmbl  46606  hoimbl  46608  opnvonmbllem2  46610  ovolval2lem  46620  ovolval2  46621  ovolval3  46624  ovolval4lem2  46627  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  ovnovollem3  46635  vonvolmbllem  46637  vonvolmbl  46638  vitali2  46671  issmflem  46704  incsmf  46719  decsmf  46744  nsssmfmbflem  46755  smfresal  46765  smfmullem4  46771  smf2id  46778  refdivpm  48472  elbigo2  48480  elbigof  48482  elbigodm  48483  elbigoimp  48484  elbigolo1  48485  prelrrx2  48641  rrx2xpref1o  48646  rrx2xpreen  48647  rrx2linesl  48671  line2  48680  line2x  48682  line2y  48683  amgmlemALT  49615