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

Theorem fndm 5685
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5596 . 2
21simprbi 464 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  domcdm 5004  Funwfun 5587  Fnwfn 5588
This theorem is referenced by:  funfni  5686  fndmu  5687  fnbr  5688  fnco  5694  fnresdm  5695  fnresdisj  5696  fnssresb  5698  fn0  5705  fnimadisj  5706  fnimaeq0  5707  dmmpti  5715  fdm  5740  f1dm  5790  f1odm  5825  f1o00  5853  fvelimab  5929  fvun1  5944  eqfnfv2  5982  fndmdif  5991  fneqeql2  5996  elpreima  6007  fsn2  6071  fnprb  6129  fnprOLD  6130  fconst3  6135  fconst4  6136  fnfvima  6150  fnunirn  6165  dff13  6166  nvof1o  6186  f1eqcocnv  6204  oprssov  6444  offval  6547  ofrfval  6548  fnexALT  6766  dmmpt2  6870  dmmpt2ga  6872  curry1  6892  curry1val  6893  curry2  6895  curry2val  6897  fparlem3  6902  fparlem4  6903  fnwelem  6915  suppvalfn  6925  suppfnss  6944  fnsuppres  6946  tposfo2  6997  smodm2  7045  smoel2  7053  tfrlem5  7068  tfrlem8  7072  tfrlem9  7073  tfrlem9a  7074  tfrlem13  7078  tfr2  7086  tz7.44-2  7092  tz7.44-3  7093  rdgsuc  7109  rdglim  7111  frsucmptn  7123  tz7.48-2  7126  tz7.48-1  7127  tz7.48-3  7128  tz7.49  7129  brwitnlem  7176  om0x  7188  oaabs2  7313  omabs  7315  elpmi  7457  elmapex  7459  pmresg  7466  pmsspw  7473  ixpprc  7510  undifixp  7525  bren  7545  fndmeng  7612  wemapso  7997  ixpiunwdom  8038  inf0  8059  noinfepOLD  8098  r1suc  8209  r1lim  8211  r1ord  8219  r1ord3  8221  jech9.3  8253  onwf  8269  ssrankr1  8274  r1val3  8277  r1pw  8284  rankuni  8302  rankr1b  8303  alephcard  8472  alephnbtwn  8473  alephgeom  8484  dfac3  8523  dfac12lem1  8544  dfac12lem2  8545  cda1dif  8577  cdacomen  8582  cdadom1  8587  cdainf  8593  pwcdadom  8617  ackbij2lem3  8642  cfsmolem  8671  alephsing  8677  fin23lem31  8744  itunisuc  8820  itunitc1  8821  ituniiun  8823  hsmexlem6  8832  zorn2lem4  8900  ttukeylem3  8912  alephadd  8973  alephreg  8978  pwcfsdom  8979  cfpwsdom  8980  r1limwun  9135  r1wunlim  9136  rankcf  9176  inatsk  9177  r1tskina  9181  grur1  9219  dmaddpi  9289  dmmulpi  9290  genpdm  9401  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  hashkf  12407  hashfn  12443  shftfn  12906  rlimi2  13337  phimullem  14309  0rest  14827  restsspw  14829  firest  14830  prdsbas2  14866  prdsplusgval  14870  prdsmulrval  14872  prdsleval  14874  prdsdsval  14875  prdsvscaval  14876  imasleval  14938  xpsfrnel2  14962  homfeqbas  15091  cidpropd  15105  2oppchomf  15119  sscpwex  15184  sscfn1  15186  sscfn2  15187  ssclem  15188  isssc  15189  rescval2  15197  issubc2  15205  cofuval  15251  resfval2  15262  resf1st  15263  resf2nd  15264  funcres  15265  fucbas  15329  fuchom  15330  xpcbas  15447  xpchomfval  15448  xpccofval  15451  oppchofcl  15529  oyoncl  15539  gsumpropd2lem  15900  frmdss2  16031  gicer  16324  psgndmsubg  16527  psgneldm  16528  psgneldm2  16529  psgnval  16532  prdsmgp  17259  lspextmo  17702  psgnghm  18616  psgnghm2  18617  dsmmbas2  18768  dsmmfi  18769  dsmmelbas  18770  frlmsslsp  18829  frlmsslspOLD  18830  islindf4  18873  ofco2  18953  cldrcl  19527  iscldtop  19596  neiss2  19602  restrcl  19658  restbas  19659  ssrest  19677  resstopn  19687  ptval  20071  txdis1cn  20136  qtopcld  20214  qtoprest  20218  kqsat  20232  kqdisj  20233  kqcldsat  20234  isr0  20238  kqnrmlem1  20244  kqnrmlem2  20245  hmphtop  20279  hmpher  20285  elfm3  20451  ustn0  20723  nghmfval  21229  isnghm  21230  ovolunlem1  21908  uniiccdif  21987  cpncn  22339  cpnres  22340  ulmf2  22779  tglngne  23937  uhgraun  24311  umgraf  24318  vdgrfval  24895  eupai  24967  eupap1  24976  ghabloOLD  25371  fcoinver  27460  ofpreima  27507  ofpreima2  27508  fnct  27536  ofcfval  28097  probfinmeasb  28368  coinflipspace  28419  cvmtop1  28705  cvmtop2  28706  dfrdg2  29228  wfrlem3  29345  wfrlem4  29346  wfrlem9  29351  wfrlem12  29354  frrlem3  29389  frrlem4  29390  frrlem5e  29395  frrlem11  29399  imageval  29580  bpolylem  29810  filnetlem4  30199  sdclem2  30235  prdstotbnd  30290  heibor1lem  30305  ismrc  30633  dnnumch3lem  30992  dnnumch3  30993  aomclem4  31003  aomclem6  31005  fnchoice  31404  fnresdmss  31443  icccncfext  31690  stoweidlem35  31817  stoweidlem59  31841  fnresfnco  32211  fnbrafvb  32239  uhgun  32380  fnxpdmdm  32456  plusfreseq  32460  bnj564  33801  bnj945  33832  bnj545  33953  bnj548  33955  bnj570  33963  bnj900  33987  bnj929  33994  bnj983  34009  bnj1018  34020  bnj1110  34038  bnj1121  34041  bnj1145  34049  bnj1245  34070  bnj1253  34073  bnj1286  34075  bnj1280  34076  bnj1296  34077  bnj1311  34080  bnj1442  34105  bnj1450  34106  bnj1498  34117  bnj1514  34119  bnj1501  34123  diadm  36762  dibdiadm  36882  dibdmN  36884  dicdmN  36911  dihdm  36996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-fn 5596
  Copyright terms: Public domain W3C validator