Theorem reex 10350

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

Assertion

Ref	Expression
reex	⊢ ℝ ∈ V

Proof of Theorem reex

Step	Hyp	Ref	Expression
1		cnex 10340	. 2 ⊢ ℂ ∈ V
2		ax-resscn 10316	. 2 ⊢ ℝ ⊆ ℂ
3	1, 2	ssexi 5030	1 ⊢ ℝ ∈ V

Syntax hints:   ∈ wcel 2164  Vcvv 3414  ℂcc 10257  ℝcr 10258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803  ax-sep 5007  ax-cnex 10315  ax-resscn 10316

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812

This theorem is referenced by:  reelprrecn  10351  negfi  11308  xrex  12116  limsuple  14593  limsuplt  14594  limsupbnd1  14597  rlim  14610  rlimf  14616  rlimss  14617  ello12  14631  lo1f  14633  lo1dm  14634  elo12  14642  o1f  14644  o1dm  14645  o1of2  14727  o1rlimmul  14733  o1add2  14738  o1mul2  14739  o1sub2  14740  o1dif  14744  caucvgrlem  14787  fsumo1  14925  rpnnen  15337  cpnnen  15339  ruclem13  15352  ruc  15353  aleph1re  15355  aleph1irr  15356  cnfldds  20123  replusg  20324  remulr  20325  rele2  20328  reds  20330  refldcj  20334  ismet  22505  tngngp2  22833  tngngpd  22834  tngngp  22835  tngngp3  22837  nrmtngnrm  22839  tngnrg  22855  rerest  22984  xrtgioo  22986  xrrest  22987  xrsmopn  22992  opnreen  23011  rectbntr0  23012  xrge0tsms  23014  bcthlem1  23499  bcthlem5  23503  reust  23556  rrxip  23565  rrx0el  23573  ehl0base  23591  ehl1eudis  23595  ehl2eudis  23597  pmltpclem2  23622  ovolficcss  23642  ovolval  23646  elovolmlem  23647  ovolctb2  23665  ismbl  23699  mblsplit  23705  voliunlem3  23725  dyadmbl  23773  vitalilem2  23782  vitalilem3  23783  vitalilem4  23784  vitalilem5  23785  vitali  23786  mbff  23798  ismbf  23801  ismbfcn  23802  mbfconst  23806  cncombf  23831  cnmbf  23832  0plef  23845  i1fd  23854  itg1ge0  23859  i1faddlem  23866  i1fmullem  23867  i1fadd  23868  i1fmul  23869  itg1addlem4  23872  i1fmulclem  23875  i1fmulc  23876  itg1mulc  23877  i1fsub  23881  itg1sub  23882  itg1lea  23885  itg1le  23886  mbfi1fseqlem2  23889  mbfi1fseqlem4  23891  mbfi1fseqlem5  23892  mbfi1flimlem  23895  mbfmullem2  23897  itg2val  23901  xrge0f  23904  itg2ge0  23908  itg2itg1  23909  itg20  23910  itg2le  23912  itg2const  23913  itg2const2  23914  itg2seq  23915  itg2uba  23916  itg2lea  23917  itg2mulclem  23919  itg2mulc  23920  itg2splitlem  23921  itg2split  23922  itg2monolem1  23923  itg2mono  23926  itg2i1fseqle  23927  itg2i1fseq  23928  itg2addlem  23931  itg2gt0  23933  itg2cnlem1  23934  itg2cnlem2  23935  iblss  23977  i1fibl  23980  itgitg1  23981  itgle  23982  ibladdlem  23992  itgaddlem1  23995  iblabslem  24000  iblabs  24001  iblabsr  24002  iblmulc2  24003  itgmulc2lem1  24004  bddmulibl  24011  dvnfre  24121  c1liplem1  24165  c1lip2  24167  lhop2  24184  dvcnvrelem2  24187  taylthlem2  24534  dmarea  25104  vmadivsum  25591  rpvmasumlem  25596  mudivsum  25639  selberglem1  25654  selberglem2  25655  selberg2lem  25659  selberg2  25660  pntrsumo1  25674  selbergr  25677  iscgrgd  25832  elee  26200  xrge0tsmsd  30326  nn0omnd  30382  xrge0slmod  30385  raddcn  30516  rrhcn  30582  qqtopn  30596  dmvlsiga  30733  ddeval1  30838  ddeval0  30839  ddemeas  30840  mbfmcnt  30871  sxbrsigalem0  30874  sxbrsigalem3  30875  sxbrsigalem2  30889  isrrvv  31047  dstfrvclim1  31081  signsplypnf  31170  erdsze2lem1  31727  erdsze2lem2  31728  snmlval  31855  knoppcnlem5  33015  knoppcnlem6  33016  knoppcnlem7  33017  knoppcnlem8  33018  cnndvlem2  33056  icoreresf  33740  icoreval  33741  poimirlem29  33977  poimirlem30  33978  poimirlem31  33979  poimir  33981  broucube  33982  mblfinlem3  33987  itg2addnclem  33999  itg2addnclem3  34001  itg2addnc  34002  itg2gt0cn  34003  ibladdnclem  34004  itgaddnclem1  34006  iblabsnclem  34011  iblabsnc  34012  iblmulc2nc  34013  itgmulc2nclem1  34014  bddiblnc  34018  ftc1anclem3  34025  ftc1anclem4  34026  ftc1anclem5  34027  ftc1anclem6  34028  ftc1anclem7  34029  ftc1anclem8  34030  ftc1anc  34031  filbcmb  34073  rrncmslem  34168  repwsmet  34170  rrnequiv  34171  ismrer1  34174  pell1qrval  38249  pell14qrval  38251  pell1234qrval  38253  k0004ss1  39284  addrval  39503  subrval  39504  mulvval  39505  climreeq  40634  limsupre  40662  limcresiooub  40663  limcresioolb  40664  limsuppnfdlem  40722  limsuppnflem  40731  limsupmnflem  40741  limsupre2lem  40745  xlimclim  40839  icccncfext  40889  cncfiooicclem1  40895  itgsubsticclem  40979  ovolsplit  40993  dirkerval  41096  dirkercncflem4  41111  fourierdlem14  41126  fourierdlem15  41127  fourierdlem32  41144  fourierdlem33  41145  fourierdlem54  41165  fourierdlem62  41173  fourierdlem70  41181  fourierdlem81  41192  fourierdlem92  41203  fourierdlem102  41213  fourierdlem111  41222  fourierdlem114  41225  etransclem2  41241  rrxtopn0  41298  qndenserrnbllem  41299  qndenserrnbl  41300  qndenserrn  41304  rrnprjdstle  41306  ioorrnopnlem  41309  dmvolsal  41349  hoicvr  41550  hoissrrn  41551  hoiprodcl2  41557  hoicvrrex  41558  ovn0lem  41567  ovn02  41570  hsphoif  41578  hoidmvval  41579  hoissrrn2  41580  hsphoival  41581  hoidmvlelem3  41599  hoidmvle  41602  ovnhoilem1  41603  ovnhoilem2  41604  ovnhoi  41605  hspval  41611  ovnlecvr2  41612  ovncvr2  41613  hoidifhspval2  41617  hoiqssbl  41627  hspmbllem2  41629  hspmbl  41631  hoimbl  41633  opnvonmbllem2  41635  ovolval2lem  41645  ovolval2  41646  ovolval3  41649  ovolval4lem2  41652  ovolval5lem2  41655  ovnovollem1  41658  ovnovollem2  41659  ovnovollem3  41660  vonvolmbllem  41662  vonvolmbl  41663  vitali2  41696  issmflem  41724  incsmf  41739  decsmf  41763  nsssmfmbflem  41774  smfresal  41783  smfmullem4  41789  smf2id  41796  prelrrx2  42273  rrx2xpref1o  42276  rrx2xpreen  42277  refdivpm  43199  elbigo2  43207  elbigof  43209  elbigodm  43210  elbigoimp  43211  elbigolo1  43212  rrx2linesl  43307  line2  43314  line2x  43316  line2y  43317  amgmlemALT  43455