Theorem reex 11179

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11169	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11145	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5283	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457  ℂcc 11086  ℝcr 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-cnex 11144  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  reelprrecn  11180  negfi  12155  xrex  13002  limsuple  15519  limsuplt  15520  limsupbnd1  15523  rlim  15536  rlimf  15542  rlimss  15543  ello12  15557  lo1f  15559  lo1dm  15560  elo12  15568  o1f  15570  o1dm  15571  o1of2  15654  o1rlimmul  15660  o1add2  15665  o1mul2  15666  o1sub2  15667  o1dif  15671  caucvgrlem  15714  fsumo1  15854  rpnnen  16273  cpnnen  16275  ruclem13  16288  ruc  16289  aleph1re  16291  aleph1irr  16292  cnfldds  21494  replusg  21720  remulr  21721  rele2  21724  reds  21726  refldcj  21730  ismet  24441  tngngp2  24770  tngngpd  24771  tngngp  24772  tngngp3  24774  nrmtngnrm  24776  tngnrg  24792  rerest  24922  xrtgioo  24925  xrrest  24926  xrsmopn  24931  opnreen  24950  rectbntr0  24951  xrge0tsms  24953  bcthlem1  25444  bcthlem5  25448  reust  25501  rrxip  25510  rrx0el  25518  ehl0base  25536  ehl1eudis  25540  ehl2eudis  25542  pmltpclem2  25569  ovolficcss  25589  ovolval  25593  elovolmlem  25594  ovolctb2  25612  ismbl  25646  mblsplit  25652  voliunlem3  25672  dyadmbl  25720  vitalilem2  25729  vitalilem3  25730  vitalilem4  25731  vitalilem5  25732  vitali  25733  mbff  25745  ismbf  25748  ismbfcn  25749  mbfconst  25753  cncombf  25778  cnmbf  25779  0plef  25792  i1fd  25801  itg1ge0  25806  i1faddlem  25813  i1fmullem  25814  i1fadd  25815  i1fmul  25816  itg1addlem4  25819  i1fmulclem  25822  i1fmulc  25823  itg1mulc  25824  i1fsub  25828  itg1sub  25829  itg1lea  25832  itg1le  25833  mbfi1fseqlem2  25836  mbfi1fseqlem4  25838  mbfi1fseqlem5  25839  mbfi1flimlem  25842  mbfmullem2  25844  itg2val  25848  xrge0f  25851  itg2ge0  25855  itg2itg1  25856  itg20  25857  itg2le  25859  itg2const  25860  itg2const2  25861  itg2seq  25862  itg2uba  25863  itg2lea  25864  itg2mulclem  25866  itg2mulc  25867  itg2splitlem  25868  itg2split  25869  itg2monolem1  25870  itg2mono  25873  itg2i1fseqle  25874  itg2i1fseq  25875  itg2addlem  25878  itg2gt0  25880  itg2cnlem1  25881  itg2cnlem2  25882  iblss  25925  i1fibl  25928  itgitg1  25929  itgle  25930  ibladdlem  25940  itgaddlem1  25943  iblabslem  25948  iblabs  25949  iblabsr  25950  iblmulc2  25951  itgmulc2lem1  25952  bddmulibl  25959  bddiblnc  25962  dvnfre  26072  c1liplem1  26116  c1lip2  26118  lhop2  26135  dvcnvrelem2  26138  taylthlem2  26495  dmarea  27080  vmadivsum  27604  rpvmasumlem  27609  mudivsum  27652  selberglem1  27667  selberglem2  27668  selberg2lem  27672  selberg2  27673  pntrsumo1  27687  selbergr  27690  iscgrgd  28740  elee  29152  xrge0tsmsd  33306  nn0omnd  33579  xrge0slmod  33583  raddcn  34236  rrhcn  34304  qqtopn  34318  dmvlsiga  34436  ddeval1  34541  ddeval0  34542  ddemeas  34543  mbfmcnt  34575  sxbrsigalem0  34578  sxbrsigalem3  34579  sxbrsigalem2  34593  isrrvv  34750  dstfrvclim1  34785  signsplypnf  34854  erdsze2lem1  35566  erdsze2lem2  35567  snmlval  35694  knoppcnlem5  36948  knoppcnlem6  36949  knoppcnlem7  36950  knoppcnlem8  36951  cnndvlem2  36989  icoreresf  37858  icoreval  37859  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimir  38164  broucube  38165  mblfinlem3  38170  itg2addnclem  38182  itg2addnclem3  38184  itg2addnc  38185  itg2gt0cn  38186  ibladdnclem  38187  itgaddnclem1  38189  iblabsnclem  38194  iblabsnc  38195  iblmulc2nc  38196  itgmulc2nclem1  38197  ftc1anclem3  38206  ftc1anclem4  38207  ftc1anclem5  38208  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  filbcmb  38251  rrncmslem  38343  repwsmet  38345  rrnequiv  38346  ismrer1  38349  absex  42876  pell1qrval  43435  pell14qrval  43437  pell1234qrval  43439  k0004ss1  44739  addrval  45039  subrval  45040  mulvval  45041  rpex  45920  climreeq  46187  limsupre  46213  limcresiooub  46214  limcresioolb  46215  limsuppnfdlem  46273  limsuppnflem  46282  limsupmnflem  46292  limsupre2lem  46296  xlimclim  46396  icccncfext  46459  cncfiooicclem1  46465  itgsubsticclem  46547  ovolsplit  46560  dirkerval  46663  dirkercncflem4  46678  fourierdlem14  46693  fourierdlem15  46694  fourierdlem32  46711  fourierdlem33  46712  fourierdlem54  46732  fourierdlem62  46740  fourierdlem70  46748  fourierdlem81  46759  fourierdlem92  46770  fourierdlem102  46780  fourierdlem111  46789  fourierdlem114  46792  etransclem2  46808  rrxtopn0  46865  qndenserrnbllem  46866  qndenserrnbl  46867  qndenserrn  46871  rrnprjdstle  46873  ioorrnopnlem  46876  dmvolsal  46918  hoicvr  47120  hoissrrn  47121  hoiprodcl2  47127  hoicvrrex  47128  ovn0lem  47137  ovn02  47140  hsphoif  47148  hoidmvval  47149  hoissrrn2  47150  hsphoival  47151  hoidmvlelem3  47169  hoidmvle  47172  ovnhoilem1  47173  ovnhoilem2  47174  ovnhoi  47175  hspval  47181  ovnlecvr2  47182  ovncvr2  47183  hoidifhspval2  47187  hoiqssbl  47197  hspmbllem2  47199  hspmbl  47201  hoimbl  47203  opnvonmbllem2  47205  ovolval2lem  47215  ovolval2  47216  ovolval3  47219  ovolval4lem2  47222  ovolval5lem2  47225  ovnovollem1  47228  ovnovollem2  47229  ovnovollem3  47230  vonvolmbllem  47232  vonvolmbl  47233  vitali2  47266  issmflem  47299  incsmf  47314  decsmf  47339  nsssmfmbflem  47350  smfresal  47360  smfmullem4  47366  smf2id  47373  nthrucw  47460  refdivpm  49175  elbigo2  49183  elbigof  49185  elbigodm  49186  elbigoimp  49187  elbigolo1  49188  prelrrx2  49344  rrx2xpref1o  49349  rrx2xpreen  49350  rrx2linesl  49374  line2  49383  line2x  49385  line2y  49386  amgmlemALT  50432