Theorem fndm 6601

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5631  Fun wfun 6492   Fn wfn 6493

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 207  df-an 396  df-fn 6501

This theorem is referenced by:  fndmi  6602  fndmd  6603  funfni  6604  fndmu  6605  fnbr  6606  fnunres1  6610  fncofn  6615  fnco  6616  fnresdm  6617  fnresdisj  6618  fnssresb  6620  fn0  6629  fnimadisj  6630  fnimaeq0  6631  f1odm  6784  fvelimab  6912  fvun1  6931  eqfnfv2  6984  fndmdif  6994  fneqeql2  6999  elpreima  7010  fsn2  7089  fnsnbg  7119  fnprb  7163  fntpb  7164  fconst3  7168  fconst4  7169  fnfvima  7188  ralima  7192  fnunirn  7208  dff13  7209  nvof1o  7235  oprssov  7536  fnexALT  7904  curry1  8054  curry1val  8055  curry2  8057  curry2val  8059  fparlem3  8064  fparlem4  8065  offsplitfpar  8069  suppvalfng  8117  suppvalfn  8118  suppfnss  8139  fnsuppres  8141  tposfo2  8199  frrlem3  8238  frrlem4  8239  smodm2  8295  smoel2  8303  tfrlem8  8323  tfrlem9  8324  tfrlem9a  8325  tfrlem13  8329  tz7.44-3  8347  rdglim  8365  frsucmptn  8378  oaabs2  8585  omabs  8587  ixpprc  8867  undifixp  8882  bren  8903  fndmeng  8982  tfsnfin2  9273  inf0  9542  r1lim  9696  jech9.3  9738  ssrankr1  9759  rankuni  9787  dfac3  10043  cfsmolem  10192  fin23lem31  10265  itunitc1  10342  ituniiun  10344  fnct  10459  cfpwsdom  10507  grur1  10743  genpdm  10925  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  hashfn  14337  cshimadifsn  14791  cshimadifsn0  14792  shftfn  15035  rlimi2  15476  phimullem  16749  restsspw  17394  prdsdsval  17441  fnpr2ob  17522  sscpwex  17782  sscfn1  17784  sscfn2  17785  isssc  17787  funcres  17863  xpcbas  18144  xpchomfval  18145  gsumpropd2lem  18647  psgndmsubg  19477  dsmmbas2  21717  dsmmelbas  21719  islindf4  21818  restbas  23123  ptval  23535  kqcldsat  23698  kqnrmlem1  23708  kqnrmlem2  23709  hmphtop  23743  ustn0  24186  uniiccdif  25545  cpncn  25903  cpnres  25904  ulmf2  26349  tglngne  28618  uhgrn0  29136  upgrfn  29156  upgrex  29161  umgrfn  29168  fcoinver  32674  fresunsn  32698  nfpconfp  32705  opprabs  33542  mdetpmtr1  33967  coinflipspace  34625  bnj945  34916  bnj545  35037  bnj548  35039  bnj570  35047  bnj900  35071  bnj929  35078  bnj983  35093  bnj1018g  35105  bnj1018  35106  bnj1110  35124  bnj1145  35135  bnj1245  35156  bnj1253  35159  bnj1286  35161  bnj1280  35162  bnj1296  35163  bnj1311  35166  bnj1450  35192  bnj1498  35203  bnj1514  35205  bnj1501  35209  dfrdg2  35975  heibor1lem  38130  aks6d1c2lem4  42566  eqresfnbd  42673  aomclem6  43487  tfsconcatun  43765  tfsconcatb0  43772  tfsconcat0i  43773  tfsconcat0b  43774  tfsconcatrev  43776  tfsnfin  43780  ntrclsfv1  44482  ntrneifv1  44506  fnresdmss  45598  dmmptif  45695  fnresfnco  47489  fnfocofob  47527  fnbrafvb  47602  uniimaprimaeqfv  47842  elsetpreimafvssdm  47846  imasetpreimafvbijlemfo  47865  fnxpdmdm  48636  plusfreseq  48640  dmdm  49528