MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reex Unicode version

Theorem reex 9604
Description: The real numbers form a set. See also reexALT 11243. (Contributed by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
reex

Proof of Theorem reex
StepHypRef Expression
1 cnex 9594 . 2
2 ax-resscn 9570 . 2
31, 2ssexi 4597 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cvv 3109   cc 9511   cr 9512
This theorem is referenced by:  reelprrecn  9605  xrex  11246  limsuple  13301  limsuplt  13302  limsupbnd1  13305  rlim  13318  rlimf  13324  rlimss  13325  ello12  13339  lo1f  13341  lo1dm  13342  elo12  13350  o1f  13352  o1dm  13353  o1of2  13435  o1rlimmul  13441  o1add2  13446  o1mul2  13447  o1sub2  13448  o1dif  13452  caucvgrlem  13495  fsumo1  13626  rpnnen  13960  cpnnen  13962  ruclem13  13975  ruc  13976  aleph1re  13978  aleph1irr  13979  cnfldds  18430  replusg  18646  remulr  18647  rele2  18650  reds  18652  refldcj  18656  ismet  20826  tngngp2  21166  tngngpd  21167  tngngp  21168  tngnrg  21183  rerest  21309  xrtgioo  21311  xrrest  21312  xrsmopn  21317  opnreen  21336  rectbntr0  21337  xrge0tsms  21339  bcthlem1  21763  bcthlem5  21767  reust  21813  rrxip  21822  pmltpclem2  21861  ovolficcss  21881  ovolval  21885  elovolm  21886  elovolmr  21887  ovolmge0  21888  ovolgelb  21891  ovolctb2  21903  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovolshftlem2  21921  ovolicc2  21933  ismbl  21937  mblsplit  21943  voliunlem3  21962  ioombl1  21972  dyadmbl  22009  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  vitalilem5  22021  vitali  22022  mbff  22034  ismbf  22037  ismbfcn  22038  mbfconst  22042  cncombf  22065  cnmbf  22066  0plef  22079  i1fd  22088  itg1ge0  22093  i1faddlem  22100  i1fmullem  22101  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulclem  22109  i1fmulc  22110  itg1mulc  22111  i1fsub  22115  itg1sub  22116  itg1lea  22119  itg1le  22120  mbfi1fseqlem2  22123  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1flimlem  22129  mbfmullem2  22131  itg2val  22135  xrge0f  22138  itg2ge0  22142  itg2itg1  22143  itg20  22144  itg2le  22146  itg2const  22147  itg2const2  22148  itg2seq  22149  itg2uba  22150  itg2lea  22151  itg2mulclem  22153  itg2mulc  22154  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq  22162  itg2addlem  22165  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  iblss  22211  i1fibl  22214  itgitg1  22215  itgle  22216  ibladdlem  22226  itgaddlem1  22229  iblabslem  22234  iblabs  22235  iblabsr  22236  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  dvnfre  22355  c1liplem1  22397  c1lip2  22399  lhop2  22416  dvcnvrelem2  22419  taylthlem2  22769  dmarea  23287  vmadivsum  23667  rpvmasumlem  23672  mudivsum  23715  selberglem1  23730  selberglem2  23731  selberg2lem  23735  selberg2  23736  pntrsumo1  23750  selbergr  23753  iscgrgd  23905  elee  24197  xrge0tsmsd  27775  nn0omnd  27831  xrge0slmod  27834  raddcn  27911  rrhcn  27978  dmvlsiga  28129  ddeval1  28206  ddeval0  28207  ddemeas  28208  mbfmcnt  28239  sxbrsigalem0  28242  sxbrsigalem3  28243  sxbrsigalem2  28257  isrrvv  28382  dstfrvclim1  28416  signsplypnf  28507  erdsze2lem1  28647  erdsze2lem2  28648  snmlval  28776  mblfinlem3  30053  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem1  30073  iblabsnclem  30078  iblabsnc  30079  iblmulc2nc  30080  itgmulc2nclem1  30081  bddiblnc  30085  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  filbcmb  30231  rrncmslem  30328  repwsmet  30330  rrnequiv  30331  ismrer1  30334  pell1qrval  30782  pell14qrval  30784  pell1234qrval  30786  addrval  31375  subrval  31376  mulvval  31377  climreeq  31619  limsupre  31647  limcresiooub  31648  limcresioolb  31649  icccncfext  31690  cncfiooicclem1  31696  itgsubsticclem  31774  dirkerval  31873  dirkercncflem4  31888  fourierdlem14  31903  fourierdlem15  31904  fourierdlem32  31921  fourierdlem33  31922  fourierdlem54  31943  fourierdlem62  31951  fourierdlem70  31959  fourierdlem81  31970  fourierdlem92  31981  fourierdlem102  31991  fourierdlem111  32000  fourierdlem114  32003  etransclem2  32019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-cnex 9569  ax-resscn 9570
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator