Theorem fndm 6288

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 6191	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 489	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1507  dom cdm 5407  Fun wfun 6182   Fn wfn 6183

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 199  df-an 388  df-fn 6191

This theorem is referenced by:  fndmd  6289  funfni  6290  fndmu  6291  fnbr  6292  fnco  6298  fnresdm  6299  fnresdisj  6300  fnssresb  6302  fn0  6309  fnimadisj  6310  fnimaeq0  6311  dmmpti  6322  fdm  6352  f1dm  6408  f1odm  6448  fvelimab  6566  fvun1  6582  eqfnfv2  6628  fndmdif  6637  fneqeql2  6642  elpreima  6653  fsn2  6721  fnprb  6797  fntpb  6798  fconst3  6802  fconst4  6803  fnfvima  6820  fnunirn  6837  dff13  6838  nvof1o  6862  f1eqcocnv  6882  oprssov  7133  fnexALT  7464  dmmpo  7577  dmmpoga  7579  curry1  7607  curry1val  7608  curry2  7610  curry2val  7612  fparlem3  7617  fparlem4  7618  fnwelem  7630  suppvalfn  7640  suppfnss  7658  fnsuppres  7660  tposfo2  7718  wfrlem3  7759  wfrlem4  7761  wfrlem4OLD  7762  wfrdmcl  7767  wfrlem12  7770  wfrlem17  7775  smodm2  7796  smoel2  7804  tfrlem5  7820  tfrlem8  7824  tfrlem9  7825  tfrlem9a  7826  tfrlem13  7830  tfr2  7838  tz7.44-2  7847  tz7.44-3  7848  rdgsuc  7864  rdglim  7866  frsucmptn  7878  tz7.48-2  7881  tz7.48-1  7882  tz7.48-3  7883  tz7.49  7884  brwitnlem  7934  om0x  7946  oaabs2  8072  omabs  8074  elpmi  8225  elmapex  8227  pmresg  8234  pmsspw  8241  ixpprc  8280  undifixp  8295  bren  8315  fndmeng  8384  ixpiunwdom  8850  inf0  8878  r1suc  8993  r1lim  8995  r1ord  9003  r1ord3  9005  jech9.3  9037  onwf  9053  ssrankr1  9058  r1val3  9061  r1pw  9068  rankuni  9086  rankr1b  9087  alephcard  9290  alephnbtwn  9291  alephgeom  9302  dfac3  9341  dfac12lem1  9363  dfac12lem2  9364  ackbij2lem3  9461  cfsmolem  9490  alephsing  9496  fin23lem31  9563  itunisuc  9639  itunitc1  9640  ituniiun  9642  hsmexlem6  9651  zorn2lem4  9719  ttukeylem3  9731  fnct  9757  alephadd  9797  alephreg  9802  pwcfsdom  9803  cfpwsdom  9804  r1limwun  9956  r1wunlim  9957  rankcf  9997  inatsk  9998  r1tskina  10002  grur1  10040  dmaddpi  10110  dmmulpi  10111  genpdm  10222  fsuppmapnn0fiublem  13173  fsuppmapnn0fiub  13174  seqexw  13200  hashkf  13507  hashfn  13549  wrdlndmOLD  13691  cshimadifsn  14053  cshimadifsn0  14054  shftfn  14293  rlimi2  14732  bpolylem  15262  phimullem  15972  0rest  16559  restsspw  16561  firest  16562  prdsbas2  16598  prdsplusgval  16602  prdsmulrval  16604  prdsleval  16606  prdsdsval  16607  prdsvscaval  16608  imasleval  16670  xpsfrnel2  16694  homfeqbas  16824  cidpropd  16838  2oppchomf  16852  sscpwex  16943  sscfn1  16945  sscfn2  16946  ssclem  16947  isssc  16948  rescval2  16956  issubc2  16964  cofuval  17010  resfval2  17021  resf1st  17022  resf2nd  17023  funcres  17024  fucbas  17088  fuchom  17089  xpcbas  17286  xpchomfval  17287  xpccofval  17290  oppchofcl  17368  oyoncl  17378  gsumpropd2lem  17741  mulgfval  18013  gicer  18187  psgndmsubg  18392  psgneldm  18393  psgneldm2  18394  psgnval  18397  prdsmgp  19083  lspextmo  19550  psgnghm  20426  psgnghm2  20427  dsmmbas2  20583  dsmmfi  20584  dsmmelbas  20585  islindf4  20684  ofco2  20764  cldrcl  21338  iscldtop  21407  neiss2  21413  restrcl  21469  restbas  21470  ssrest  21488  resstopn  21498  ptval  21882  txdis1cn  21947  qtopcld  22025  qtoprest  22029  kqsat  22043  kqdisj  22044  kqcldsat  22045  isr0  22049  kqnrmlem1  22055  kqnrmlem2  22056  hmphtop  22090  hmpher  22096  elfm3  22262  ustn0  22532  nghmfval  23034  isnghm  23035  ovolunlem1  23801  uniiccdif  23882  cpncn  24236  cpnres  24237  ulmf2  24675  tglngne  26038  uhgrn0  26555  upgrfn  26575  upgrex  26580  umgrfn  26587  fnunres1  30120  fcoinver  30121  ofpreima  30172  ofpreima2  30173  fnpreimac  30178  mdetpmtr1  30736  probfinmeasb  31339  coinflipspace  31390  bnj564  31669  bnj945  31699  bnj545  31820  bnj548  31822  bnj570  31830  bnj900  31854  bnj929  31861  bnj983  31876  bnj1018  31887  bnj1110  31905  bnj1145  31916  bnj1245  31937  bnj1253  31940  bnj1286  31942  bnj1280  31943  bnj1296  31944  bnj1311  31947  bnj1442  31972  bnj1450  31973  bnj1498  31984  bnj1514  31986  bnj1501  31990  cvmtop1  32098  cvmtop2  32099  dfrdg2  32567  frrlem3  32652  frrlem4  32653  frrlem8  32657  frrlem10  32659  imageval  32918  filnetlem4  33256  sdclem2  34465  prdstotbnd  34520  heibor1lem  34535  dibdiadm  37742  dibdmN  37744  dicdmN  37771  dihdm  37856  fnsnbt  38571  ismrc  38699  dnnumch3lem  39048  dnnumch3  39049  aomclem4  39059  aomclem6  39061  ntrclsfv1  39774  ntrneifv1  39798  grur1cld  39949  fnresdmss  40854  icccncfext  41606  stoweidlem35  41757  stoweidlem59  41781  fnresfnco  42687  fnbrafvb  42765  fnxpdmdm  43409  plusfreseq  43413