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

Theorem fndm 5343
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 5258 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 450 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   dom cdm 4689   Fun wfun 5249    Fn wfn 5250
This theorem is referenced by:  funfni  5344  fndmu  5345  fnbr  5346  fnco  5352  fnresdm  5353  fnresdisj  5354  fnssresb  5356  fn0  5363  fnimadisj  5364  fnimaeq0  5365  dmmpti  5373  fdm  5393  f1dm  5441  f1odm  5476  f1o00  5508  fvelimab  5578  fvun1  5590  eqfnfv2  5623  fndmdif  5629  fneqeql2  5634  elpreima  5645  fsn2  5698  fconst3  5735  fconst4  5736  fnexALT  5742  fnfvima  5756  fnunirn  5778  dff13  5783  f1eqcocnv  5805  oprssov  5989  offval  6085  ofrfval  6086  dmmpt2  6194  curry1  6210  curry1val  6211  curry2  6213  curry2val  6215  fparlem3  6220  fparlem4  6221  fnwelem  6230  tposfo2  6257  smodm2  6372  smoel2  6380  tfrlem8  6400  tfrlem9  6401  tfrlem9a  6402  tfrlem13  6406  tfr2  6414  tz7.44-2  6420  tz7.44-3  6421  rdgsuc  6437  rdglim  6439  frsucmptn  6451  tz7.48-2  6454  tz7.48-1  6455  tz7.48-3  6456  tz7.49  6457  brwitnlem  6506  om0x  6518  oaabs2  6643  omabs  6645  elpmi  6789  elmapex  6791  pmresg  6795  pmsspw  6802  ixpprc  6837  undifixp  6852  bren  6871  fndmeng  6937  wemapso  7266  ixpiunwdom  7305  inf0  7322  noinfepOLD  7361  r1suc  7442  r1lim  7444  r1ord  7452  r1ord3  7454  jech9.3  7486  onwf  7502  ssrankr1  7507  r1val3  7510  r1pw  7517  rankuni  7535  rankr1b  7536  alephcard  7697  alephnbtwn  7698  alephgeom  7709  dfac3  7748  dfac12lem1  7769  dfac12lem2  7770  cda1dif  7802  cdacomen  7807  cdadom1  7812  cdainf  7818  pwcdadom  7842  ackbij2lem3  7867  cfsmolem  7896  alephsing  7902  fin23lem31  7969  itunisuc  8045  itunitc1  8046  ituniiun  8048  hsmexlem6  8057  zorn2lem4  8126  ttukeylem3  8138  alephadd  8199  alephreg  8204  pwcfsdom  8205  cfpwsdom  8206  r1limwun  8358  r1wunlim  8359  rankcf  8399  inatsk  8400  r1tskina  8404  grur1  8442  dmaddpi  8514  dmmulpi  8515  genpdm  8626  hashkf  11339  hashfn  11357  shftfn  11568  rlimi2  11988  rlimmptrcl  12081  phimullem  12847  0rest  13334  restsspw  13336  firest  13337  prdsbas2  13368  prdsplusgval  13372  prdsmulrval  13374  prdsleval  13376  prdsdsval  13377  prdsvscaval  13378  imasleval  13443  xpsfrnel2  13467  homfeqbas  13599  cidpropd  13613  2oppchomf  13627  sscpwex  13692  sscfn1  13694  sscfn2  13695  ssclem  13696  isssc  13697  rescval2  13705  issubc2  13713  cofuval  13756  resfval2  13767  resf1st  13768  resf2nd  13769  funcres  13770  fullfunc  13780  fthfunc  13781  natfval  13820  fucbas  13834  fuchom  13835  xpcbas  13952  xpchomfval  13953  xpccofval  13956  oppchofcl  14034  oyoncl  14044  frmdss2  14485  gicer  14740  prdsmgp  15393  lspextmo  15813  cldrcl  16763  iscldtop  16832  neiss2  16838  restrcl  16888  restbas  16889  ssrest  16907  resstopn  16916  ptval  17265  txdis1cn  17329  qtopcld  17404  qtoprest  17408  kqsat  17422  kqdisj  17423  kqcldsat  17424  isr0  17428  kqnrmlem1  17434  kqnrmlem2  17435  hmphtop  17469  hmpher  17475  elfm3  17645  nghmfval  18231  isnghm  18232  ovolunlem1  18856  uniiccdif  18933  iblcnlem  19143  cpncn  19285  cpnres  19286  dvmptres3  19305  ulmf2  19763  ghablo  21036  nvof1o  23036  fnct  23341  gsumpropd2lem  23379  ofcfval  23459  indf1ofs  23609  probfinmeasb  23632  coinflipspace  23681  cvmtop1  23791  cvmtop2  23792  umgraf  23870  eupai  23883  vdgrfval  23889  eupap1  23900  dfrdg2  24152  wfrlem3  24258  wfrlem4  24259  wfrlem9  24264  wfrlem12  24267  frrlem3  24283  frrlem4  24284  frrlem5e  24289  frrlem11  24293  imageval  24469  bpolylem  24783  imfstnrelc  25081  npincppr  25159  repfuntw  25160  prl2  25169  cur1vald  25199  domrancur1b  25200  domrancur1c  25202  valcurfn1  25204  nsn  25530  valdom  25884  fnctartar  25907  fnctartar2  25908  filnetlem4  26330  sdclem2  26452  prdstotbnd  26518  heibor1lem  26533  ismrc  26776  dnnumch3lem  27143  dnnumch3  27144  aomclem4  27154  aomclem6  27156  dsmmbas2  27203  dsmmfi  27204  dsmmelbas  27205  frlmsslsp  27248  frlmlbs  27249  islindf4  27308  psgndmsubg  27425  psgneldm  27426  psgneldm2  27427  psgnval  27430  psgnghm  27437  psgnghm2  27438  fnchoice  27700  stoweidlem35  27784  stoweidlem59  27808  dmmpt2g  27981  fnresfnco  27989  fnbrafvb  28016  bnj564  28773  bnj945  28805  bnj545  28927  bnj548  28929  bnj570  28937  bnj900  28961  bnj929  28968  bnj983  28983  bnj1018  28994  bnj1110  29012  bnj1121  29015  bnj1145  29023  bnj1245  29044  bnj1253  29047  bnj1286  29049  bnj1280  29050  bnj1296  29051  bnj1311  29054  bnj1442  29079  bnj1450  29080  bnj1498  29091  bnj1514  29093  bnj1501  29097  diadm  31225  dibdiadm  31345  dibdmN  31347  dicdmN  31374  dihdm  31459
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 5258
  Copyright terms: Public domain W3C validator