Theorem fndm 6682

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700  Fun wfun 6567   Fn wfn 6568

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 6576

This theorem is referenced by:  fndmi  6683  fndmd  6684  funfni  6685  fndmu  6686  fnbr  6687  fnunres1  6691  fncofn  6696  fnco  6697  fncoOLD  6698  fnresdm  6699  fnresdisj  6700  fnssresb  6702  fn0  6711  fnimadisj  6712  fnimaeq0  6713  f1odm  6866  fvelimab  6994  fvun1  7013  eqfnfv2  7065  fndmdif  7075  fneqeql2  7080  elpreima  7091  fsn2  7170  fnprb  7245  fntpb  7246  fconst3  7250  fconst4  7251  fnfvima  7270  ralima  7274  fnunirn  7291  dff13  7292  nvof1o  7316  oprssov  7619  fnexALT  7991  curry1  8145  curry1val  8146  curry2  8148  curry2val  8150  fparlem3  8155  fparlem4  8156  offsplitfpar  8160  suppvalfng  8208  suppvalfn  8209  suppfnss  8230  fnsuppres  8232  tposfo2  8290  frrlem3  8329  frrlem4  8330  wfrlem3OLD  8366  wfrlem4OLD  8368  wfrdmclOLD  8373  wfrlem12OLD  8376  smodm2  8411  smoel2  8419  tfrlem8  8440  tfrlem9  8441  tfrlem9a  8442  tfrlem13  8446  tz7.44-3  8464  rdglim  8482  frsucmptn  8495  oaabs2  8705  omabs  8707  ixpprc  8977  undifixp  8992  bren  9013  brenOLD  9014  fndmeng  9100  inf0  9690  r1lim  9841  jech9.3  9883  ssrankr1  9904  rankuni  9932  dfac3  10190  cfsmolem  10339  fin23lem31  10412  itunitc1  10489  ituniiun  10491  fnct  10606  cfpwsdom  10653  grur1  10889  genpdm  11071  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  hashfn  14424  cshimadifsn  14878  cshimadifsn0  14879  shftfn  15122  rlimi2  15560  phimullem  16826  restsspw  17491  prdsdsval  17538  fnpr2ob  17618  sscpwex  17876  sscfn1  17878  sscfn2  17879  isssc  17881  funcres  17960  xpcbas  18247  xpchomfval  18248  gsumpropd2lem  18717  psgndmsubg  19544  dsmmbas2  21780  dsmmelbas  21782  islindf4  21881  restbas  23187  ptval  23599  kqcldsat  23762  kqnrmlem1  23772  kqnrmlem2  23773  hmphtop  23807  ustn0  24250  uniiccdif  25632  cpncn  25992  cpnres  25993  ulmf2  26445  tglngne  28576  uhgrn0  29102  upgrfn  29122  upgrex  29127  umgrfn  29134  fcoinver  32626  nfpconfp  32651  opprabs  33475  mdetpmtr1  33769  coinflipspace  34445  bnj945  34749  bnj545  34871  bnj548  34873  bnj570  34881  bnj900  34905  bnj929  34912  bnj983  34927  bnj1018g  34939  bnj1018  34940  bnj1110  34958  bnj1145  34969  bnj1245  34990  bnj1253  34993  bnj1286  34995  bnj1280  34996  bnj1296  34997  bnj1311  35000  bnj1450  35026  bnj1498  35037  bnj1514  35039  bnj1501  35043  dfrdg2  35759  heibor1lem  37769  aks6d1c2lem4  42084  fnsnbt  42225  eqresfnbd  42227  aomclem6  43016  tfsconcatun  43299  tfsconcatb0  43306  tfsconcat0i  43307  tfsconcat0b  43308  tfsconcatrev  43310  tfsnfin  43314  ntrclsfv1  44017  ntrneifv1  44041  fnresdmss  45075  dmmptif  45176  fnresfnco  46956  fnfocofob  46994  fnbrafvb  47069  uniimaprimaeqfv  47256  elsetpreimafvssdm  47260  imasetpreimafvbijlemfo  47279  fnxpdmdm  47883  plusfreseq  47887