Theorem reex 11275

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11265	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11241	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5340	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ℂcc 11182  ℝcr 11183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  reelprrecn  11276  negfi  12244  xrex  13052  limsuple  15524  limsuplt  15525  limsupbnd1  15528  rlim  15541  rlimf  15547  rlimss  15548  ello12  15562  lo1f  15564  lo1dm  15565  elo12  15573  o1f  15575  o1dm  15576  o1of2  15659  o1rlimmul  15665  o1add2  15670  o1mul2  15671  o1sub2  15672  o1dif  15676  caucvgrlem  15721  fsumo1  15860  rpnnen  16275  cpnnen  16277  ruclem13  16290  ruc  16291  aleph1re  16293  aleph1irr  16294  cnfldds  21399  cnflddsOLD  21412  replusg  21651  remulr  21652  rele2  21655  reds  21657  refldcj  21661  ismet  24354  tngngp2  24694  tngngpd  24695  tngngp  24696  tngngp3  24698  nrmtngnrm  24700  tngnrg  24716  rerest  24845  xrtgioo  24847  xrrest  24848  xrsmopn  24853  opnreen  24872  rectbntr0  24873  xrge0tsms  24875  bcthlem1  25377  bcthlem5  25381  reust  25434  rrxip  25443  rrx0el  25451  ehl0base  25469  ehl1eudis  25473  ehl2eudis  25475  pmltpclem2  25503  ovolficcss  25523  ovolval  25527  elovolmlem  25528  ovolctb2  25546  ismbl  25580  mblsplit  25586  voliunlem3  25606  dyadmbl  25654  vitalilem2  25663  vitalilem3  25664  vitalilem4  25665  vitalilem5  25666  vitali  25667  mbff  25679  ismbf  25682  ismbfcn  25683  mbfconst  25687  cncombf  25712  cnmbf  25713  0plef  25726  i1fd  25735  itg1ge0  25740  i1faddlem  25747  i1fmullem  25748  i1fadd  25749  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  i1fmulclem  25757  i1fmulc  25758  itg1mulc  25759  i1fsub  25763  itg1sub  25764  itg1lea  25767  itg1le  25768  mbfi1fseqlem2  25771  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1flimlem  25777  mbfmullem2  25779  itg2val  25783  xrge0f  25786  itg2ge0  25790  itg2itg1  25791  itg20  25792  itg2le  25794  itg2const  25795  itg2const2  25796  itg2seq  25797  itg2uba  25798  itg2lea  25799  itg2mulclem  25801  itg2mulc  25802  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2addlem  25813  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  iblss  25860  i1fibl  25863  itgitg1  25864  itgle  25865  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgmulc2lem1  25887  bddmulibl  25894  bddiblnc  25897  dvnfre  26010  c1liplem1  26055  c1lip2  26057  lhop2  26074  dvcnvrelem2  26077  taylthlem2  26434  taylthlem2OLD  26435  dmarea  27018  vmadivsum  27544  rpvmasumlem  27549  mudivsum  27592  selberglem1  27607  selberglem2  27608  selberg2lem  27612  selberg2  27613  pntrsumo1  27627  selbergr  27630  iscgrgd  28539  elee  28927  xrge0tsmsd  33041  nn0omnd  33338  xrge0slmod  33341  raddcn  33875  rrhcn  33943  qqtopn  33957  dmvlsiga  34093  ddeval1  34198  ddeval0  34199  ddemeas  34200  mbfmcnt  34233  sxbrsigalem0  34236  sxbrsigalem3  34237  sxbrsigalem2  34251  isrrvv  34408  dstfrvclim1  34442  signsplypnf  34527  erdsze2lem1  35171  erdsze2lem2  35172  snmlval  35299  knoppcnlem5  36463  knoppcnlem6  36464  knoppcnlem7  36465  knoppcnlem8  36466  cnndvlem2  36504  icoreresf  37318  icoreval  37319  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimir  37613  broucube  37614  mblfinlem3  37619  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ibladdnclem  37636  itgaddnclem1  37638  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nclem1  37646  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  filbcmb  37700  rrncmslem  37792  repwsmet  37794  rrnequiv  37795  ismrer1  37798  absex  42243  pell1qrval  42802  pell14qrval  42804  pell1234qrval  42806  k0004ss1  44113  addrval  44435  subrval  44436  mulvval  44437  climreeq  45534  limsupre  45562  limcresiooub  45563  limcresioolb  45564  limsuppnfdlem  45622  limsuppnflem  45631  limsupmnflem  45641  limsupre2lem  45645  xlimclim  45745  icccncfext  45808  cncfiooicclem1  45814  itgsubsticclem  45896  ovolsplit  45909  dirkerval  46012  dirkercncflem4  46027  fourierdlem14  46042  fourierdlem15  46043  fourierdlem32  46060  fourierdlem33  46061  fourierdlem54  46081  fourierdlem62  46089  fourierdlem70  46097  fourierdlem81  46108  fourierdlem92  46119  fourierdlem102  46129  fourierdlem111  46138  fourierdlem114  46141  etransclem2  46157  rrxtopn0  46214  qndenserrnbllem  46215  qndenserrnbl  46216  qndenserrn  46220  rrnprjdstle  46222  ioorrnopnlem  46225  dmvolsal  46267  hoicvr  46469  hoissrrn  46470  hoiprodcl2  46476  hoicvrrex  46477  ovn0lem  46486  ovn02  46489  hsphoif  46497  hoidmvval  46498  hoissrrn2  46499  hsphoival  46500  hoidmvlelem3  46518  hoidmvle  46521  ovnhoilem1  46522  ovnhoilem2  46523  ovnhoi  46524  hspval  46530  ovnlecvr2  46531  ovncvr2  46532  hoidifhspval2  46536  hoiqssbl  46546  hspmbllem2  46548  hspmbl  46550  hoimbl  46552  opnvonmbllem2  46554  ovolval2lem  46564  ovolval2  46565  ovolval3  46568  ovolval4lem2  46571  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  ovnovollem3  46579  vonvolmbllem  46581  vonvolmbl  46582  vitali2  46615  issmflem  46648  incsmf  46663  decsmf  46688  nsssmfmbflem  46699  smfresal  46709  smfmullem4  46715  smf2id  46722  refdivpm  48278  elbigo2  48286  elbigof  48288  elbigodm  48289  elbigoimp  48290  elbigolo1  48291  prelrrx2  48447  rrx2xpref1o  48452  rrx2xpreen  48453  rrx2linesl  48477  line2  48486  line2x  48488  line2y  48489  amgmlemALT  48897