Theorem reex 11187

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11177	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11153	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5290	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ℂcc 11094  ℝcr 11095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-cnex 11152  ax-resscn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930

This theorem is referenced by:  reelprrecn  11188  negfi  12160  xrex  13007  limsuple  15525  limsuplt  15526  limsupbnd1  15529  rlim  15542  rlimf  15548  rlimss  15549  ello12  15563  lo1f  15565  lo1dm  15566  elo12  15574  o1f  15576  o1dm  15577  o1of2  15660  o1rlimmul  15666  o1add2  15671  o1mul2  15672  o1sub2  15673  o1dif  15677  caucvgrlem  15720  fsumo1  15860  rpnnen  16279  cpnnen  16281  ruclem13  16294  ruc  16295  aleph1re  16297  aleph1irr  16298  cnfldds  21499  replusg  21725  remulr  21726  rele2  21729  reds  21731  refldcj  21735  ismet  24445  tngngp2  24774  tngngpd  24775  tngngp  24776  tngngp3  24778  nrmtngnrm  24780  tngnrg  24796  rerest  24926  xrtgioo  24929  xrrest  24930  xrsmopn  24935  opnreen  24954  rectbntr0  24955  xrge0tsms  24957  bcthlem1  25448  bcthlem5  25452  reust  25505  rrxip  25514  rrx0el  25522  ehl0base  25540  ehl1eudis  25544  ehl2eudis  25546  pmltpclem2  25573  ovolficcss  25593  ovolval  25597  elovolmlem  25598  ovolctb2  25616  ismbl  25650  mblsplit  25656  voliunlem3  25676  dyadmbl  25724  vitalilem2  25733  vitalilem3  25734  vitalilem4  25735  vitalilem5  25736  vitali  25737  mbff  25749  ismbf  25752  ismbfcn  25753  mbfconst  25757  cncombf  25782  cnmbf  25783  0plef  25796  i1fd  25805  itg1ge0  25810  i1faddlem  25817  i1fmullem  25818  i1fadd  25819  i1fmul  25820  itg1addlem4  25823  i1fmulclem  25826  i1fmulc  25827  itg1mulc  25828  i1fsub  25832  itg1sub  25833  itg1lea  25836  itg1le  25837  mbfi1fseqlem2  25840  mbfi1fseqlem4  25842  mbfi1fseqlem5  25843  mbfi1flimlem  25846  mbfmullem2  25848  itg2val  25852  xrge0f  25855  itg2ge0  25859  itg2itg1  25860  itg20  25861  itg2le  25863  itg2const  25864  itg2const2  25865  itg2seq  25866  itg2uba  25867  itg2lea  25868  itg2mulclem  25870  itg2mulc  25871  itg2splitlem  25872  itg2split  25873  itg2monolem1  25874  itg2mono  25877  itg2i1fseqle  25878  itg2i1fseq  25879  itg2addlem  25882  itg2gt0  25884  itg2cnlem1  25885  itg2cnlem2  25886  iblss  25929  i1fibl  25932  itgitg1  25933  itgle  25934  ibladdlem  25944  itgaddlem1  25947  iblabslem  25952  iblabs  25953  iblabsr  25954  iblmulc2  25955  itgmulc2lem1  25956  bddmulibl  25963  bddiblnc  25966  dvnfre  26076  c1liplem1  26120  c1lip2  26122  lhop2  26139  dvcnvrelem2  26142  taylthlem2  26499  dmarea  27084  vmadivsum  27608  rpvmasumlem  27613  mudivsum  27656  selberglem1  27671  selberglem2  27672  selberg2lem  27676  selberg2  27677  pntrsumo1  27691  selbergr  27694  iscgrgd  28744  elee  29180  xrge0tsmsd  33330  nn0omnd  33603  xrge0slmod  33607  raddcn  34260  rrhcn  34328  qqtopn  34342  dmvlsiga  34460  ddeval1  34565  ddeval0  34566  ddemeas  34567  mbfmcnt  34599  sxbrsigalem0  34602  sxbrsigalem3  34603  sxbrsigalem2  34617  isrrvv  34774  dstfrvclim1  34809  signsplypnf  34878  erdsze2lem1  35590  erdsze2lem2  35591  snmlval  35718  knoppcnlem5  36971  knoppcnlem6  36972  knoppcnlem7  36973  knoppcnlem8  36974  cnndvlem2  37012  icoreresf  37881  icoreval  37882  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  poimir  38187  broucube  38188  mblfinlem3  38193  itg2addnclem  38205  itg2addnclem3  38207  itg2addnc  38208  itg2gt0cn  38209  ibladdnclem  38210  itgaddnclem1  38212  iblabsnclem  38217  iblabsnc  38218  iblmulc2nc  38219  itgmulc2nclem1  38220  ftc1anclem3  38229  ftc1anclem4  38230  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  filbcmb  38274  rrncmslem  38366  repwsmet  38368  rrnequiv  38369  ismrer1  38372  absex  42899  pell1qrval  43458  pell14qrval  43460  pell1234qrval  43462  k0004ss1  44762  addrval  45059  subrval  45060  mulvval  45061  rpex  45947  climreeq  46214  limsupre  46240  limcresiooub  46241  limcresioolb  46242  limsuppnfdlem  46300  limsuppnflem  46309  limsupmnflem  46319  limsupre2lem  46323  xlimclim  46423  icccncfext  46486  cncfiooicclem1  46492  itgsubsticclem  46574  ovolsplit  46587  dirkerval  46690  dirkercncflem4  46705  fourierdlem14  46720  fourierdlem15  46721  fourierdlem32  46738  fourierdlem33  46739  fourierdlem54  46759  fourierdlem62  46767  fourierdlem70  46775  fourierdlem81  46786  fourierdlem92  46797  fourierdlem102  46807  fourierdlem111  46816  fourierdlem114  46819  etransclem2  46835  rrxtopn0  46892  qndenserrnbllem  46893  qndenserrnbl  46894  qndenserrn  46898  rrnprjdstle  46900  ioorrnopnlem  46903  dmvolsal  46945  hoicvr  47147  hoissrrn  47148  hoiprodcl2  47154  hoicvrrex  47155  ovn0lem  47164  ovn02  47167  hsphoif  47175  hoidmvval  47176  hoissrrn2  47177  hsphoival  47178  hoidmvlelem3  47196  hoidmvle  47199  ovnhoilem1  47200  ovnhoilem2  47201  ovnhoi  47202  hspval  47208  ovnlecvr2  47209  ovncvr2  47210  hoidifhspval2  47214  hoiqssbl  47224  hspmbllem2  47226  hspmbl  47228  hoimbl  47230  opnvonmbllem2  47232  ovolval2lem  47242  ovolval2  47243  ovolval3  47246  ovolval4lem2  47249  ovolval5lem2  47252  ovnovollem1  47255  ovnovollem2  47256  ovnovollem3  47257  vonvolmbllem  47259  vonvolmbl  47260  vitali2  47293  issmflem  47326  incsmf  47341  decsmf  47366  nsssmfmbflem  47377  smfresal  47387  smfmullem4  47393  smf2id  47400  nthrucw  47487  refdivpm  49202  elbigo2  49210  elbigof  49212  elbigodm  49213  elbigoimp  49214  elbigolo1  49215  prelrrx2  49371  rrx2xpref1o  49376  rrx2xpreen  49377  rrx2linesl  49401  line2  49410  line2x  49412  line2y  49413  amgmlemALT  50459