Theorem reex 11235

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 11225	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11201	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5324	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2098  Vcvv 3471  ℂcc 11142  ℝcr 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698  ax-sep 5301  ax-cnex 11200  ax-resscn 11201

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  reelprrecn  11236  negfi  12199  xrex  13007  limsuple  15460  limsuplt  15461  limsupbnd1  15464  rlim  15477  rlimf  15483  rlimss  15484  ello12  15498  lo1f  15500  lo1dm  15501  elo12  15509  o1f  15511  o1dm  15512  o1of2  15595  o1rlimmul  15601  o1add2  15606  o1mul2  15607  o1sub2  15608  o1dif  15612  caucvgrlem  15657  fsumo1  15796  rpnnen  16209  cpnnen  16211  ruclem13  16224  ruc  16225  aleph1re  16227  aleph1irr  16228  cnfldds  21296  cnflddsOLD  21309  replusg  21547  remulr  21548  rele2  21551  reds  21553  refldcj  21557  ismet  24247  tngngp2  24587  tngngpd  24588  tngngp  24589  tngngp3  24591  nrmtngnrm  24593  tngnrg  24609  rerest  24738  xrtgioo  24740  xrrest  24741  xrsmopn  24746  opnreen  24765  rectbntr0  24766  xrge0tsms  24768  bcthlem1  25270  bcthlem5  25274  reust  25327  rrxip  25336  rrx0el  25344  ehl0base  25362  ehl1eudis  25366  ehl2eudis  25368  pmltpclem2  25396  ovolficcss  25416  ovolval  25420  elovolmlem  25421  ovolctb2  25439  ismbl  25473  mblsplit  25479  voliunlem3  25499  dyadmbl  25547  vitalilem2  25556  vitalilem3  25557  vitalilem4  25558  vitalilem5  25559  vitali  25560  mbff  25572  ismbf  25575  ismbfcn  25576  mbfconst  25580  cncombf  25605  cnmbf  25606  0plef  25619  i1fd  25628  itg1ge0  25633  i1faddlem  25640  i1fmullem  25641  i1fadd  25642  i1fmul  25643  itg1addlem4  25646  itg1addlem4OLD  25647  i1fmulclem  25650  i1fmulc  25651  itg1mulc  25652  i1fsub  25656  itg1sub  25657  itg1lea  25660  itg1le  25661  mbfi1fseqlem2  25664  mbfi1fseqlem4  25666  mbfi1fseqlem5  25667  mbfi1flimlem  25670  mbfmullem2  25672  itg2val  25676  xrge0f  25679  itg2ge0  25683  itg2itg1  25684  itg20  25685  itg2le  25687  itg2const  25688  itg2const2  25689  itg2seq  25690  itg2uba  25691  itg2lea  25692  itg2mulclem  25694  itg2mulc  25695  itg2splitlem  25696  itg2split  25697  itg2monolem1  25698  itg2mono  25701  itg2i1fseqle  25702  itg2i1fseq  25703  itg2addlem  25706  itg2gt0  25708  itg2cnlem1  25709  itg2cnlem2  25710  iblss  25752  i1fibl  25755  itgitg1  25756  itgle  25757  ibladdlem  25767  itgaddlem1  25770  iblabslem  25775  iblabs  25776  iblabsr  25777  iblmulc2  25778  itgmulc2lem1  25779  bddmulibl  25786  bddiblnc  25789  dvnfre  25902  c1liplem1  25947  c1lip2  25949  lhop2  25966  dvcnvrelem2  25969  taylthlem2  26327  taylthlem2OLD  26328  dmarea  26907  vmadivsum  27433  rpvmasumlem  27438  mudivsum  27481  selberglem1  27496  selberglem2  27497  selberg2lem  27501  selberg2  27502  pntrsumo1  27516  selbergr  27519  iscgrgd  28335  elee  28723  xrge0tsmsd  32789  nn0omnd  33075  xrge0slmod  33078  raddcn  33535  rrhcn  33603  qqtopn  33617  dmvlsiga  33753  ddeval1  33858  ddeval0  33859  ddemeas  33860  mbfmcnt  33893  sxbrsigalem0  33896  sxbrsigalem3  33897  sxbrsigalem2  33911  isrrvv  34068  dstfrvclim1  34102  signsplypnf  34187  erdsze2lem1  34818  erdsze2lem2  34819  snmlval  34946  knoppcnlem5  35977  knoppcnlem6  35978  knoppcnlem7  35979  knoppcnlem8  35980  cnndvlem2  36018  icoreresf  36836  icoreval  36837  poimirlem29  37127  poimirlem30  37128  poimirlem31  37129  poimir  37131  broucube  37132  mblfinlem3  37137  itg2addnclem  37149  itg2addnclem3  37151  itg2addnc  37152  itg2gt0cn  37153  ibladdnclem  37154  itgaddnclem1  37156  iblabsnclem  37161  iblabsnc  37162  iblmulc2nc  37163  itgmulc2nclem1  37164  ftc1anclem3  37173  ftc1anclem4  37174  ftc1anclem5  37175  ftc1anclem6  37176  ftc1anclem7  37177  ftc1anclem8  37178  ftc1anc  37179  filbcmb  37218  rrncmslem  37310  repwsmet  37312  rrnequiv  37313  ismrer1  37316  pell1qrval  42269  pell14qrval  42271  pell1234qrval  42273  k0004ss1  43584  addrval  43906  subrval  43907  mulvval  43908  climreeq  45003  limsupre  45031  limcresiooub  45032  limcresioolb  45033  limsuppnfdlem  45091  limsuppnflem  45100  limsupmnflem  45110  limsupre2lem  45114  xlimclim  45214  icccncfext  45277  cncfiooicclem1  45283  itgsubsticclem  45365  ovolsplit  45378  dirkerval  45481  dirkercncflem4  45496  fourierdlem14  45511  fourierdlem15  45512  fourierdlem32  45529  fourierdlem33  45530  fourierdlem54  45550  fourierdlem62  45558  fourierdlem70  45566  fourierdlem81  45577  fourierdlem92  45588  fourierdlem102  45598  fourierdlem111  45607  fourierdlem114  45610  etransclem2  45626  rrxtopn0  45683  qndenserrnbllem  45684  qndenserrnbl  45685  qndenserrn  45689  rrnprjdstle  45691  ioorrnopnlem  45694  dmvolsal  45736  hoicvr  45938  hoissrrn  45939  hoiprodcl2  45945  hoicvrrex  45946  ovn0lem  45955  ovn02  45958  hsphoif  45966  hoidmvval  45967  hoissrrn2  45968  hsphoival  45969  hoidmvlelem3  45987  hoidmvle  45990  ovnhoilem1  45991  ovnhoilem2  45992  ovnhoi  45993  hspval  45999  ovnlecvr2  46000  ovncvr2  46001  hoidifhspval2  46005  hoiqssbl  46015  hspmbllem2  46017  hspmbl  46019  hoimbl  46021  opnvonmbllem2  46023  ovolval2lem  46033  ovolval2  46034  ovolval3  46037  ovolval4lem2  46040  ovolval5lem2  46043  ovnovollem1  46046  ovnovollem2  46047  ovnovollem3  46048  vonvolmbllem  46050  vonvolmbl  46051  vitali2  46084  issmflem  46117  incsmf  46132  decsmf  46157  nsssmfmbflem  46168  smfresal  46178  smfmullem4  46184  smf2id  46191  refdivpm  47668  elbigo2  47676  elbigof  47678  elbigodm  47679  elbigoimp  47680  elbigolo1  47681  prelrrx2  47837  rrx2xpref1o  47842  rrx2xpreen  47843  rrx2linesl  47867  line2  47876  line2x  47878  line2y  47879  amgmlemALT  48287