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

Theorem fndm 5678
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm  |-  ( F  Fn  A  ->  dom  F  =  A )

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5589 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 464 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   dom cdm 4999   Fun wfun 5580    Fn wfn 5581
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 5589
This theorem is referenced by:  funfni  5679  fndmu  5680  fnbr  5681  fnco  5687  fnresdm  5688  fnresdisj  5689  fnssresb  5691  fn0  5698  fnimadisj  5699  fnimaeq0  5700  dmmpti  5708  fdm  5733  f1dm  5783  f1odm  5818  f1o00  5846  fvelimab  5921  fvun1  5936  eqfnfv2  5974  fndmdif  5983  fneqeql2  5988  elpreima  5999  fsn2  6059  fnprb  6117  fnprOLD  6118  fconst3  6122  fconst4  6123  fnfvima  6136  fnunirn  6151  dff13  6152  nvof1o  6172  f1eqcocnv  6190  oprssov  6426  offval  6529  ofrfval  6530  fnexALT  6747  dmmpt2  6851  dmmpt2ga  6852  curry1  6872  curry1val  6873  curry2  6875  curry2val  6877  fparlem3  6882  fparlem4  6883  fnwelem  6895  suppvalfn  6905  suppfnss  6922  fnsuppres  6924  tposfo2  6975  smodm2  7023  smoel2  7031  tfrlem5  7046  tfrlem8  7050  tfrlem9  7051  tfrlem9a  7052  tfrlem13  7056  tfr2  7064  tz7.44-2  7070  tz7.44-3  7071  rdgsuc  7087  rdglim  7089  frsucmptn  7101  tz7.48-2  7104  tz7.48-1  7105  tz7.48-3  7106  tz7.49  7107  brwitnlem  7154  om0x  7166  oaabs2  7291  omabs  7293  elpmi  7434  elmapex  7436  pmresg  7443  pmsspw  7450  ixpprc  7487  undifixp  7502  bren  7522  fndmeng  7589  wemapso  7972  ixpiunwdom  8013  inf0  8034  noinfepOLD  8073  r1suc  8184  r1lim  8186  r1ord  8194  r1ord3  8196  jech9.3  8228  onwf  8244  ssrankr1  8249  r1val3  8252  r1pw  8259  rankuni  8277  rankr1b  8278  alephcard  8447  alephnbtwn  8448  alephgeom  8459  dfac3  8498  dfac12lem1  8519  dfac12lem2  8520  cda1dif  8552  cdacomen  8557  cdadom1  8562  cdainf  8568  pwcdadom  8592  ackbij2lem3  8617  cfsmolem  8646  alephsing  8652  fin23lem31  8719  itunisuc  8795  itunitc1  8796  ituniiun  8798  hsmexlem6  8807  zorn2lem4  8875  ttukeylem3  8887  alephadd  8948  alephreg  8953  pwcfsdom  8954  cfpwsdom  8955  r1limwun  9110  r1wunlim  9111  rankcf  9151  inatsk  9152  r1tskina  9156  grur1  9194  dmaddpi  9264  dmmulpi  9265  genpdm  9376  fsuppmapnn0fiublem  12059  fsuppmapnn0fiub  12060  hashkf  12369  hashfn  12405  shftfn  12863  rlimi2  13293  rlimmptrcl  13386  phimullem  14161  0rest  14678  restsspw  14680  firest  14681  prdsbas2  14717  prdsplusgval  14721  prdsmulrval  14723  prdsleval  14725  prdsdsval  14726  prdsvscaval  14727  imasleval  14789  xpsfrnel2  14813  homfeqbas  14945  cidpropd  14959  2oppchomf  14973  sscpwex  15038  sscfn1  15040  sscfn2  15041  ssclem  15042  isssc  15043  rescval2  15051  issubc2  15059  cofuval  15102  resfval2  15113  resf1st  15114  resf2nd  15115  funcres  15116  fucbas  15180  fuchom  15181  xpcbas  15298  xpchomfval  15299  xpccofval  15302  oppchofcl  15380  oyoncl  15390  gsumpropd2lem  15815  frmdss2  15851  gicer  16116  psgndmsubg  16320  psgneldm  16321  psgneldm2  16322  psgnval  16325  prdsmgp  17040  lspextmo  17482  psgnghm  18380  psgnghm2  18381  dsmmbas2  18532  dsmmfi  18533  dsmmelbas  18534  frlmsslsp  18593  frlmsslspOLD  18594  islindf4  18637  ofco2  18717  cldrcl  19290  iscldtop  19359  neiss2  19365  restrcl  19421  restbas  19422  ssrest  19440  resstopn  19450  ptval  19803  txdis1cn  19868  qtopcld  19946  qtoprest  19950  kqsat  19964  kqdisj  19965  kqcldsat  19966  isr0  19970  kqnrmlem1  19976  kqnrmlem2  19977  hmphtop  20011  hmpher  20017  elfm3  20183  ustn0  20455  nghmfval  20961  isnghm  20962  ovolunlem1  21640  uniiccdif  21719  iblcnlem  21927  cpncn  22071  cpnres  22072  dvmptres3  22091  ulmf2  22510  tglngne  23662  uhgraun  23984  umgraf  23991  vdgrfval  24568  eupai  24640  eupap1  24649  ghablo  25044  fcoinver  27130  ofpreima  27176  ofpreima2  27177  fnct  27205  ofcfval  27734  sseqf  27968  probfinmeasb  28005  coinflipspace  28056  cvmtop1  28342  cvmtop2  28343  dfrdg2  28802  wfrlem3  28919  wfrlem4  28920  wfrlem9  28925  wfrlem12  28928  frrlem3  28963  frrlem4  28964  frrlem5e  28969  frrlem11  28973  imageval  29154  bpolylem  29384  filnetlem4  29800  sdclem2  29836  prdstotbnd  29891  heibor1lem  29906  ismrc  30235  dnnumch3lem  30596  dnnumch3  30597  aomclem4  30607  aomclem6  30609  fnchoice  30982  fnresdmss  31021  icccncfext  31226  stoweidlem35  31335  stoweidlem59  31359  fnresfnco  31678  fnbrafvb  31706  uhgun  31849  fnxpdmdm  31959  bnj564  32880  bnj945  32911  bnj545  33032  bnj548  33034  bnj570  33042  bnj900  33066  bnj929  33073  bnj983  33088  bnj1018  33099  bnj1110  33117  bnj1121  33120  bnj1145  33128  bnj1245  33149  bnj1253  33152  bnj1286  33154  bnj1280  33155  bnj1296  33156  bnj1311  33159  bnj1442  33184  bnj1450  33185  bnj1498  33196  bnj1514  33198  bnj1501  33202  diadm  35832  dibdiadm  35952  dibdmN  35954  dicdmN  35981  dihdm  36066
  Copyright terms: Public domain W3C validator