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

Theorem fndm 5546
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 5459 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 452 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   dom cdm 4880   Fun wfun 5450    Fn wfn 5451
This theorem is referenced by:  funfni  5547  fndmu  5548  fnbr  5549  fnco  5555  fnresdm  5556  fnresdisj  5557  fnssresb  5559  fn0  5566  fnimadisj  5567  fnimaeq0  5568  dmmpti  5576  fdm  5597  f1dm  5645  f1odm  5680  f1o00  5712  fvelimab  5784  fvun1  5796  eqfnfv2  5830  fndmdif  5836  fneqeql2  5841  elpreima  5852  fsn2  5910  fnpr  5952  fnprOLD  5953  fconst3  5957  fconst4  5958  fnexALT  5964  fnfvima  5978  fnunirn  6001  dff13  6006  f1eqcocnv  6030  oprssov  6217  offval  6314  ofrfval  6315  dmmpt2  6423  curry1  6440  curry1val  6441  curry2  6443  curry2val  6445  fparlem3  6450  fparlem4  6451  fnwelem  6463  tposfo2  6504  smodm2  6619  smoel2  6627  tfrlem8  6647  tfrlem9  6648  tfrlem9a  6649  tfrlem13  6653  tfr2  6661  tz7.44-2  6667  tz7.44-3  6668  rdgsuc  6684  rdglim  6686  frsucmptn  6698  tz7.48-2  6701  tz7.48-1  6702  tz7.48-3  6703  tz7.49  6704  brwitnlem  6753  om0x  6765  oaabs2  6890  omabs  6892  elpmi  7037  elmapex  7039  pmresg  7043  pmsspw  7050  ixpprc  7085  undifixp  7100  bren  7119  fndmeng  7185  wemapso  7522  ixpiunwdom  7561  inf0  7578  noinfepOLD  7617  r1suc  7698  r1lim  7700  r1ord  7708  r1ord3  7710  jech9.3  7742  onwf  7758  ssrankr1  7763  r1val3  7766  r1pw  7773  rankuni  7791  rankr1b  7792  alephcard  7953  alephnbtwn  7954  alephgeom  7965  dfac3  8004  dfac12lem1  8025  dfac12lem2  8026  cda1dif  8058  cdacomen  8063  cdadom1  8068  cdainf  8074  pwcdadom  8098  ackbij2lem3  8123  cfsmolem  8152  alephsing  8158  fin23lem31  8225  itunisuc  8301  itunitc1  8302  ituniiun  8304  hsmexlem6  8313  zorn2lem4  8381  ttukeylem3  8393  alephadd  8454  alephreg  8459  pwcfsdom  8460  cfpwsdom  8461  r1limwun  8613  r1wunlim  8614  rankcf  8654  inatsk  8655  r1tskina  8659  grur1  8697  dmaddpi  8769  dmmulpi  8770  genpdm  8881  hashkf  11622  hashfn  11651  shftfn  11890  rlimi2  12310  rlimmptrcl  12403  phimullem  13170  0rest  13659  restsspw  13661  firest  13662  prdsbas2  13693  prdsplusgval  13697  prdsmulrval  13699  prdsleval  13701  prdsdsval  13702  prdsvscaval  13703  imasleval  13768  xpsfrnel2  13792  homfeqbas  13924  cidpropd  13938  2oppchomf  13952  sscpwex  14017  sscfn1  14019  sscfn2  14020  ssclem  14021  isssc  14022  rescval2  14030  issubc2  14038  cofuval  14081  resfval2  14092  resf1st  14093  resf2nd  14094  funcres  14095  fucbas  14159  fuchom  14160  xpcbas  14277  xpchomfval  14278  xpccofval  14281  oppchofcl  14359  oyoncl  14369  frmdss2  14810  gicer  15065  prdsmgp  15718  lspextmo  16134  cldrcl  17092  iscldtop  17161  neiss2  17167  restrcl  17223  restbas  17224  ssrest  17242  resstopn  17252  ptval  17604  txdis1cn  17669  qtopcld  17747  qtoprest  17751  kqsat  17765  kqdisj  17766  kqcldsat  17767  isr0  17771  kqnrmlem1  17777  kqnrmlem2  17778  hmphtop  17812  hmpher  17818  elfm3  17984  ustn0  18252  nghmfval  18758  isnghm  18759  ovolunlem1  19395  uniiccdif  19472  iblcnlem  19682  cpncn  19824  cpnres  19825  dvmptres3  19844  ulmf2  20302  uhgraun  21348  umgraf  21355  vdgrfval  21668  eupai  21691  eupap1  21700  ghablo  21959  nvof1o  24042  ofpreima  24083  fnct  24107  gsumpropd2lem  24222  ofcfval  24483  probfinmeasb  24689  coinflipspace  24740  cvmtop1  24949  cvmtop2  24950  dfrdg2  25425  wfrlem3  25542  wfrlem4  25543  wfrlem9  25548  wfrlem12  25551  frrlem3  25586  frrlem4  25587  frrlem5e  25592  frrlem11  25596  imageval  25777  bpolylem  26096  filnetlem4  26412  sdclem2  26448  prdstotbnd  26505  heibor1lem  26520  ismrc  26757  dnnumch3lem  27123  dnnumch3  27124  aomclem4  27134  aomclem6  27136  dsmmbas2  27182  dsmmfi  27183  dsmmelbas  27184  frlmsslsp  27227  frlmlbs  27228  islindf4  27287  psgndmsubg  27404  psgneldm  27405  psgneldm2  27406  psgnval  27409  psgnghm  27416  psgnghm2  27417  fnchoice  27678  stoweidlem35  27762  stoweidlem59  27786  dmmpt2g  27961  fnresfnco  27968  fnbrafvb  27996  bnj564  29174  bnj945  29206  bnj545  29328  bnj548  29330  bnj570  29338  bnj900  29362  bnj929  29369  bnj983  29384  bnj1018  29395  bnj1110  29413  bnj1121  29416  bnj1145  29424  bnj1245  29445  bnj1253  29448  bnj1286  29450  bnj1280  29451  bnj1296  29452  bnj1311  29455  bnj1442  29480  bnj1450  29481  bnj1498  29492  bnj1514  29494  bnj1501  29498  diadm  31895  dibdiadm  32015  dibdmN  32017  dicdmN  32044  dihdm  32129
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 179  df-an 362  df-fn 5459
  Copyright terms: Public domain W3C validator