Theorem reex 11158

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 11148	. 2 ⊢ ℂ ∈ V
2		ax-resscn 11124	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5275	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ℂcc 11065  ℝcr 11066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-cnex 11123  ax-resscn 11124

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-in 3909  df-ss 3919

This theorem is referenced by:  reelprrecn  11159  negfi  12135  xrex  12982  limsuple  15496  limsuplt  15497  limsupbnd1  15500  rlim  15513  rlimf  15519  rlimss  15520  ello12  15534  lo1f  15536  lo1dm  15537  elo12  15545  o1f  15547  o1dm  15548  o1of2  15631  o1rlimmul  15637  o1add2  15642  o1mul2  15643  o1sub2  15644  o1dif  15648  caucvgrlem  15691  fsumo1  15831  rpnnen  16250  cpnnen  16252  ruclem13  16265  ruc  16266  aleph1re  16268  aleph1irr  16269  cnfldds  21424  replusg  21650  remulr  21651  rele2  21654  reds  21656  refldcj  21660  ismet  24371  tngngp2  24700  tngngpd  24701  tngngp  24702  tngngp3  24704  nrmtngnrm  24706  tngnrg  24722  rerest  24852  xrtgioo  24855  xrrest  24856  xrsmopn  24861  opnreen  24880  rectbntr0  24881  xrge0tsms  24883  bcthlem1  25374  bcthlem5  25378  reust  25431  rrxip  25440  rrx0el  25448  ehl0base  25466  ehl1eudis  25470  ehl2eudis  25472  pmltpclem2  25499  ovolficcss  25519  ovolval  25523  elovolmlem  25524  ovolctb2  25542  ismbl  25576  mblsplit  25582  voliunlem3  25602  dyadmbl  25650  vitalilem2  25659  vitalilem3  25660  vitalilem4  25661  vitalilem5  25662  vitali  25663  mbff  25675  ismbf  25678  ismbfcn  25679  mbfconst  25683  cncombf  25708  cnmbf  25709  0plef  25722  i1fd  25731  itg1ge0  25736  i1faddlem  25743  i1fmullem  25744  i1fadd  25745  i1fmul  25746  itg1addlem4  25749  i1fmulclem  25752  i1fmulc  25753  itg1mulc  25754  i1fsub  25758  itg1sub  25759  itg1lea  25762  itg1le  25763  mbfi1fseqlem2  25766  mbfi1fseqlem4  25768  mbfi1fseqlem5  25769  mbfi1flimlem  25772  mbfmullem2  25774  itg2val  25778  xrge0f  25781  itg2ge0  25785  itg2itg1  25786  itg20  25787  itg2le  25789  itg2const  25790  itg2const2  25791  itg2seq  25792  itg2uba  25793  itg2lea  25794  itg2mulclem  25796  itg2mulc  25797  itg2splitlem  25798  itg2split  25799  itg2monolem1  25800  itg2mono  25803  itg2i1fseqle  25804  itg2i1fseq  25805  itg2addlem  25808  itg2gt0  25810  itg2cnlem1  25811  itg2cnlem2  25812  iblss  25855  i1fibl  25858  itgitg1  25859  itgle  25860  ibladdlem  25870  itgaddlem1  25873  iblabslem  25878  iblabs  25879  iblabsr  25880  iblmulc2  25881  itgmulc2lem1  25882  bddmulibl  25889  bddiblnc  25892  dvnfre  26002  c1liplem1  26046  c1lip2  26048  lhop2  26065  dvcnvrelem2  26068  taylthlem2  26425  dmarea  27010  vmadivsum  27534  rpvmasumlem  27539  mudivsum  27582  selberglem1  27597  selberglem2  27598  selberg2lem  27602  selberg2  27603  pntrsumo1  27617  selbergr  27620  iscgrgd  28670  elee  29051  xrge0tsmsd  33214  nn0omnd  33491  xrge0slmod  33495  raddcn  34187  rrhcn  34255  qqtopn  34269  dmvlsiga  34387  ddeval1  34492  ddeval0  34493  ddemeas  34494  mbfmcnt  34526  sxbrsigalem0  34529  sxbrsigalem3  34530  sxbrsigalem2  34544  isrrvv  34701  dstfrvclim1  34736  signsplypnf  34805  erdsze2lem1  35514  erdsze2lem2  35515  snmlval  35642  knoppcnlem5  36896  knoppcnlem6  36897  knoppcnlem7  36898  knoppcnlem8  36899  cnndvlem2  36937  icoreresf  37807  icoreval  37808  poimirlem29  38109  poimirlem30  38110  poimirlem31  38111  poimir  38113  broucube  38114  mblfinlem3  38119  itg2addnclem  38131  itg2addnclem3  38133  itg2addnc  38134  itg2gt0cn  38135  ibladdnclem  38136  itgaddnclem1  38138  iblabsnclem  38143  iblabsnc  38144  iblmulc2nc  38145  itgmulc2nclem1  38146  ftc1anclem3  38155  ftc1anclem4  38156  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  filbcmb  38200  rrncmslem  38292  repwsmet  38294  rrnequiv  38295  ismrer1  38298  absex  42825  pell1qrval  43384  pell14qrval  43386  pell1234qrval  43388  k0004ss1  44688  addrval  45002  subrval  45003  mulvval  45004  rpex  45883  climreeq  46150  limsupre  46176  limcresiooub  46177  limcresioolb  46178  limsuppnfdlem  46236  limsuppnflem  46245  limsupmnflem  46255  limsupre2lem  46259  xlimclim  46359  icccncfext  46422  cncfiooicclem1  46428  itgsubsticclem  46510  ovolsplit  46523  dirkerval  46626  dirkercncflem4  46641  fourierdlem14  46656  fourierdlem15  46657  fourierdlem32  46674  fourierdlem33  46675  fourierdlem54  46695  fourierdlem62  46703  fourierdlem70  46711  fourierdlem81  46722  fourierdlem92  46733  fourierdlem102  46743  fourierdlem111  46752  fourierdlem114  46755  etransclem2  46771  rrxtopn0  46828  qndenserrnbllem  46829  qndenserrnbl  46830  qndenserrn  46834  rrnprjdstle  46836  ioorrnopnlem  46839  dmvolsal  46881  hoicvr  47083  hoissrrn  47084  hoiprodcl2  47090  hoicvrrex  47091  ovn0lem  47100  ovn02  47103  hsphoif  47111  hoidmvval  47112  hoissrrn2  47113  hsphoival  47114  hoidmvlelem3  47132  hoidmvle  47135  ovnhoilem1  47136  ovnhoilem2  47137  ovnhoi  47138  hspval  47144  ovnlecvr2  47145  ovncvr2  47146  hoidifhspval2  47150  hoiqssbl  47160  hspmbllem2  47162  hspmbl  47164  hoimbl  47166  opnvonmbllem2  47168  ovolval2lem  47178  ovolval2  47179  ovolval3  47182  ovolval4lem2  47185  ovolval5lem2  47188  ovnovollem1  47191  ovnovollem2  47192  ovnovollem3  47193  vonvolmbllem  47195  vonvolmbl  47196  vitali2  47229  issmflem  47262  incsmf  47277  decsmf  47302  nsssmfmbflem  47313  smfresal  47323  smfmullem4  47329  smf2id  47336  nthrucw  47423  refdivpm  49127  elbigo2  49135  elbigof  49137  elbigodm  49138  elbigoimp  49139  elbigolo1  49140  prelrrx2  49296  rrx2xpref1o  49301  rrx2xpreen  49302  rrx2linesl  49326  line2  49335  line2x  49337  line2y  49338  amgmlemALT  50385