Theorem fndm 5990

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

Step	Hyp	Ref	Expression
1		df-fn 5891	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simprbi 480	1 |- ( F Fn A -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1483   dom cdm 5114   Fun wfun 5882   Fn wfn 5883

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 197  df-an 386  df-fn 5891

This theorem is referenced by:  funfni  5991  fndmu  5992  fnbr  5993  fnco  5999  fnresdm  6000  fnresdisj  6001  fnssresb  6003  fn0  6011  fnimadisj  6012  fnimaeq0  6013  dmmpti  6023  fdm  6051  f1dm  6105  f1odm  6141  f1o00  6171  fvelimab  6253  fvun1  6269  eqfnfv2  6312  fndmdif  6321  fneqeql2  6326  elpreima  6337  fsn2  6403  fnprb  6472  fntpb  6473  fconst3  6477  fconst4  6478  fnfvima  6496  fnunirn  6511  dff13  6512  nvof1o  6536  f1eqcocnv  6556  oprssov  6803  offval  6904  ofrfval  6905  fnexALT  7132  dmmpt2  7240  dmmpt2ga  7242  curry1  7269  curry1val  7270  curry2  7272  curry2val  7274  fparlem3  7279  fparlem4  7280  fnwelem  7292  suppvalfn  7302  suppfnss  7320  fnsuppres  7322  tposfo2  7375  wfrlem3  7416  wfrlem4  7418  wfrdmcl  7423  wfrlem12  7426  wfrlem17  7431  smodm2  7452  smoel2  7460  tfrlem5  7476  tfrlem8  7480  tfrlem9  7481  tfrlem9a  7482  tfrlem13  7486  tfr2  7494  tz7.44-2  7503  tz7.44-3  7504  rdgsuc  7520  rdglim  7522  frsucmptn  7534  tz7.48-2  7537  tz7.48-1  7538  tz7.48-3  7539  tz7.49  7540  brwitnlem  7587  om0x  7599  oaabs2  7725  omabs  7727  elpmi  7876  elmapex  7878  pmresg  7885  pmsspw  7892  ixpprc  7929  undifixp  7944  bren  7964  fndmeng  8034  wemapso  8456  ixpiunwdom  8496  inf0  8518  r1suc  8633  r1lim  8635  r1ord  8643  r1ord3  8645  jech9.3  8677  onwf  8693  ssrankr1  8698  r1val3  8701  r1pw  8708  rankuni  8726  rankr1b  8727  alephcard  8893  alephnbtwn  8894  alephgeom  8905  dfac3  8944  dfac12lem1  8965  dfac12lem2  8966  cda1dif  8998  cdacomen  9003  cdadom1  9008  cdainf  9014  pwcdadom  9038  ackbij2lem3  9063  cfsmolem  9092  alephsing  9098  fin23lem31  9165  itunisuc  9241  itunitc1  9242  ituniiun  9244  hsmexlem6  9253  zorn2lem4  9321  ttukeylem3  9333  fnct  9359  alephadd  9399  alephreg  9404  pwcfsdom  9405  cfpwsdom  9406  r1limwun  9558  r1wunlim  9559  rankcf  9599  inatsk  9600  r1tskina  9604  grur1  9642  dmaddpi  9712  dmmulpi  9713  genpdm  9824  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  hashkf  13119  hashfn  13164  wrdlndm  13321  cshimadifsn  13575  cshimadifsn0  13576  shftfn  13813  rlimi2  14245  bpolylem  14779  phimullem  15484  0rest  16090  restsspw  16092  firest  16093  prdsbas2  16129  prdsplusgval  16133  prdsmulrval  16135  prdsleval  16137  prdsdsval  16138  prdsvscaval  16139  imasleval  16201  xpsfrnel2  16225  homfeqbas  16356  cidpropd  16370  2oppchomf  16384  sscpwex  16475  sscfn1  16477  sscfn2  16478  ssclem  16479  isssc  16480  rescval2  16488  issubc2  16496  cofuval  16542  resfval2  16553  resf1st  16554  resf2nd  16555  funcres  16556  fucbas  16620  fuchom  16621  xpcbas  16818  xpchomfval  16819  xpccofval  16822  oppchofcl  16900  oyoncl  16910  gsumpropd2lem  17273  frmdss2  17400  gicer  17718  gicerOLD  17719  psgndmsubg  17922  psgneldm  17923  psgneldm2  17924  psgnval  17927  prdsmgp  18610  lspextmo  19056  psgnghm  19926  psgnghm2  19927  dsmmbas2  20081  dsmmfi  20082  dsmmelbas  20083  frlmsslsp  20135  islindf4  20177  ofco2  20257  cldrcl  20830  iscldtop  20899  neiss2  20905  restrcl  20961  restbas  20962  ssrest  20980  resstopn  20990  ptval  21373  txdis1cn  21438  qtopcld  21516  qtoprest  21520  kqsat  21534  kqdisj  21535  kqcldsat  21536  isr0  21540  kqnrmlem1  21546  kqnrmlem2  21547  hmphtop  21581  hmpher  21587  elfm3  21754  ustn0  22024  nghmfval  22526  isnghm  22527  ovolunlem1  23265  uniiccdif  23346  cpncn  23699  cpnres  23700  ulmf2  24138  tglngne  25445  uhgrn0  25962  upgrfn  25982  upgrex  25987  umgrfn  25994  fnunres1  29417  fcoinver  29418  ofpreima  29465  ofpreima2  29466  mdetpmtr1  29889  ofcfval  30160  probfinmeasb  30491  coinflipspace  30542  bnj564  30814  bnj945  30844  bnj545  30965  bnj548  30967  bnj570  30975  bnj900  30999  bnj929  31006  bnj983  31021  bnj1018  31032  bnj1110  31050  bnj1121  31053  bnj1145  31061  bnj1245  31082  bnj1253  31085  bnj1286  31087  bnj1280  31088  bnj1296  31089  bnj1311  31092  bnj1442  31117  bnj1450  31118  bnj1498  31129  bnj1514  31131  bnj1501  31135  cvmtop1  31242  cvmtop2  31243  dfrdg2  31701  frrlem3  31782  frrlem4  31783  frrlem5e  31788  frrlem11  31792  imageval  32037  filnetlem4  32376  sdclem2  33538  prdstotbnd  33593  heibor1lem  33608  diadm  36324  dibdiadm  36444  dibdmN  36446  dicdmN  36473  dihdm  36558  ismrc  37264  dnnumch3lem  37616  dnnumch3  37617  aomclem4  37627  aomclem6  37629  ntrclsfv1  38353  ntrneifv1  38377  fnchoice  39188  fnresdmss  39348  wessf1ornlem  39371  fndmd  39441  icccncfext  40100  stoweidlem35  40252  stoweidlem59  40276  fnresfnco  41206  fnbrafvb  41234  fnxpdmdm  41768  plusfreseq  41772