Theorem fndm 5904

Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fndm	⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 5807	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 479	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1475  dom cdm 5038  Fun wfun 5798   Fn wfn 5799

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 196  df-an 385  df-fn 5807

This theorem is referenced by:  funfni  5905  fndmu  5906  fnbr  5907  fnco  5913  fnresdm  5914  fnresdisj  5915  fnssresb  5917  fn0  5924  fnimadisj  5925  fnimaeq0  5926  dmmpti  5936  fdm  5964  f1dm  6018  f1odm  6054  f1o00  6083  fvelimab  6163  fvun1  6179  eqfnfv2  6220  fndmdif  6229  fneqeql2  6234  elpreima  6245  fsn2  6309  fnprb  6377  fntpb  6378  fconst3  6382  fconst4  6383  fnfvima  6400  fnunirn  6415  dff13  6416  nvof1o  6436  f1eqcocnv  6456  oprssov  6701  offval  6802  ofrfval  6803  fnexALT  7025  dmmpt2  7129  dmmpt2ga  7131  curry1  7156  curry1val  7157  curry2  7159  curry2val  7161  fparlem3  7166  fparlem4  7167  fnwelem  7179  suppvalfn  7189  suppfnss  7207  fnsuppres  7209  tposfo2  7262  wfrlem3  7303  wfrlem4  7305  wfrdmcl  7310  wfrlem12  7313  wfrlem17  7318  smodm2  7339  smoel2  7347  tfrlem5  7363  tfrlem8  7367  tfrlem9  7368  tfrlem9a  7369  tfrlem13  7373  tfr2  7381  tz7.44-2  7390  tz7.44-3  7391  rdgsuc  7407  rdglim  7409  frsucmptn  7421  tz7.48-2  7424  tz7.48-1  7425  tz7.48-3  7426  tz7.49  7427  brwitnlem  7474  om0x  7486  oaabs2  7612  omabs  7614  elpmi  7762  elmapex  7764  pmresg  7771  pmsspw  7778  ixpprc  7815  undifixp  7830  bren  7850  fndmeng  7919  wemapso  8339  ixpiunwdom  8379  inf0  8401  r1suc  8516  r1lim  8518  r1ord  8526  r1ord3  8528  jech9.3  8560  onwf  8576  ssrankr1  8581  r1val3  8584  r1pw  8591  rankuni  8609  rankr1b  8610  alephcard  8776  alephnbtwn  8777  alephgeom  8788  dfac3  8827  dfac12lem1  8848  dfac12lem2  8849  cda1dif  8881  cdacomen  8886  cdadom1  8891  cdainf  8897  pwcdadom  8921  ackbij2lem3  8946  cfsmolem  8975  alephsing  8981  fin23lem31  9048  itunisuc  9124  itunitc1  9125  ituniiun  9127  hsmexlem6  9136  zorn2lem4  9204  ttukeylem3  9216  alephadd  9278  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  r1limwun  9437  r1wunlim  9438  rankcf  9478  inatsk  9479  r1tskina  9483  grur1  9521  dmaddpi  9591  dmmulpi  9592  genpdm  9703  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  hashkf  12981  hashfn  13025  wrdlndm  13176  cshimadifsn  13426  cshimadifsn0  13427  shftfn  13661  rlimi2  14093  bpolylem  14618  phimullem  15322  0rest  15913  restsspw  15915  firest  15916  prdsbas2  15952  prdsplusgval  15956  prdsmulrval  15958  prdsleval  15960  prdsdsval  15961  prdsvscaval  15962  imasleval  16024  xpsfrnel2  16048  homfeqbas  16179  cidpropd  16193  2oppchomf  16207  sscpwex  16298  sscfn1  16300  sscfn2  16301  ssclem  16302  isssc  16303  rescval2  16311  issubc2  16319  cofuval  16365  resfval2  16376  resf1st  16377  resf2nd  16378  funcres  16379  fucbas  16443  fuchom  16444  xpcbas  16641  xpchomfval  16642  xpccofval  16645  oppchofcl  16723  oyoncl  16733  gsumpropd2lem  17096  frmdss2  17223  gicer  17541  gicerOLD  17542  psgndmsubg  17745  psgneldm  17746  psgneldm2  17747  psgnval  17750  prdsmgp  18433  lspextmo  18877  psgnghm  19745  psgnghm2  19746  dsmmbas2  19900  dsmmfi  19901  dsmmelbas  19902  frlmsslsp  19954  islindf4  19996  ofco2  20076  cldrcl  20640  iscldtop  20709  neiss2  20715  restrcl  20771  restbas  20772  ssrest  20790  resstopn  20800  ptval  21183  txdis1cn  21248  qtopcld  21326  qtoprest  21330  kqsat  21344  kqdisj  21345  kqcldsat  21346  isr0  21350  kqnrmlem1  21356  kqnrmlem2  21357  hmphtop  21391  hmpher  21397  elfm3  21564  ustn0  21834  nghmfval  22336  isnghm  22337  ovolunlem1  23072  uniiccdif  23152  cpncn  23505  cpnres  23506  ulmf2  23942  tglngne  25245  uhgrn0  25733  upgrfn  25754  upgrex  25759  umgrfn  25765  uhgraun  25840  umgraf  25847  vdgrfval  26422  eupai  26494  eupap1  26503  fcoinver  28798  ofpreima  28848  ofpreima2  28849  fnct  28876  mdetpmtr1  29217  ofcfval  29487  probfinmeasb  29818  coinflipspace  29869  bnj564  30068  bnj945  30098  bnj545  30219  bnj548  30221  bnj570  30229  bnj900  30253  bnj929  30260  bnj983  30275  bnj1018  30286  bnj1110  30304  bnj1121  30307  bnj1145  30315  bnj1245  30336  bnj1253  30339  bnj1286  30341  bnj1280  30342  bnj1296  30343  bnj1311  30346  bnj1442  30371  bnj1450  30372  bnj1498  30383  bnj1514  30385  bnj1501  30389  cvmtop1  30496  cvmtop2  30497  dfrdg2  30945  frrlem3  31026  frrlem4  31027  frrlem5e  31032  frrlem11  31036  imageval  31207  filnetlem4  31546  sdclem2  32708  prdstotbnd  32763  heibor1lem  32778  diadm  35342  dibdiadm  35462  dibdmN  35464  dicdmN  35491  dihdm  35576  ismrc  36282  dnnumch3lem  36634  dnnumch3  36635  aomclem4  36645  aomclem6  36647  ntrclsfv1  37373  ntrneifv1  37397  fnchoice  38211  fnresdmss  38342  wessf1ornlem  38366  icccncfext  38773  stoweidlem35  38928  stoweidlem59  38952  fnresfnco  39855  fnbrafvb  39883  fnxpdmdm  41558  plusfreseq  41562