Theorem fndm 6481

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

Syntax hints:   → wi 4   = wceq 1543  dom cdm 5551  Fun wfun 6374   Fn wfn 6375

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 210  df-an 400  df-fn 6383

This theorem is referenced by:  fndmi  6482  fndmd  6483  funfni  6484  fndmu  6485  fnbr  6486  fncofn  6493  fnco  6494  fncoOLD  6495  fnresdm  6496  fnresdisj  6497  fnssresb  6499  fn0  6509  fnimadisj  6510  fnimaeq0  6511  fdmOLD  6555  f1dmOLD  6620  f1odm  6665  fvelimab  6784  fvun1  6802  eqfnfv2  6853  fndmdif  6862  fneqeql2  6867  elpreima  6878  fsn2  6951  fnprb  7024  fntpb  7025  fconst3  7029  fconst4  7030  fnfvima  7049  fnunirn  7066  dff13  7067  nvof1o  7091  f1eqcocnvOLD  7112  oprssov  7377  fnexALT  7724  dmmpogaOLD  7844  curry1  7872  curry1val  7873  curry2  7875  curry2val  7877  fparlem3  7882  fparlem4  7883  offsplitfpar  7888  suppvalfng  7910  suppvalfn  7911  suppfnss  7931  fnsuppres  7933  tposfo2  7991  frrlem3  8029  frrlem4  8030  wfrlem3  8056  wfrlem4  8058  wfrdmcl  8063  wfrlem12  8066  smodm2  8092  smoel2  8100  tfrlem8  8120  tfrlem9  8121  tfrlem9a  8122  tfrlem13  8126  tz7.44-3  8144  rdglim  8162  frsucmptn  8174  oaabs2  8374  omabs  8376  ixpprc  8600  undifixp  8615  bren  8636  brenOLD  8637  fndmeng  8712  inf0  9236  r1lim  9388  jech9.3  9430  ssrankr1  9451  rankuni  9479  dfac3  9735  cfsmolem  9884  fin23lem31  9957  itunitc1  10034  ituniiun  10036  fnct  10151  cfpwsdom  10198  grur1  10434  genpdm  10616  fsuppmapnn0fiublem  13563  fsuppmapnn0fiub  13564  hashfn  13942  cshimadifsn  14394  cshimadifsn0  14395  shftfn  14636  rlimi2  15075  phimullem  16332  restsspw  16936  prdsdsval  16983  fnpr2ob  17063  sscpwex  17320  sscfn1  17322  sscfn2  17323  isssc  17325  funcres  17402  xpcbas  17685  xpchomfval  17686  gsumpropd2lem  18151  psgndmsubg  18894  dsmmbas2  20699  dsmmelbas  20701  islindf4  20800  restbas  22055  ptval  22467  kqcldsat  22630  kqnrmlem1  22640  kqnrmlem2  22641  hmphtop  22675  ustn0  23118  uniiccdif  24475  cpncn  24833  cpnres  24834  ulmf2  25276  tglngne  26641  uhgrn0  27158  upgrfn  27178  upgrex  27183  umgrfn  27190  fnunres1  30664  fcoinver  30665  nfpconfp  30686  mdetpmtr1  31487  coinflipspace  32159  bnj945  32466  bnj545  32588  bnj548  32590  bnj570  32598  bnj900  32622  bnj929  32629  bnj983  32644  bnj1018g  32656  bnj1018  32657  bnj1110  32675  bnj1145  32686  bnj1245  32707  bnj1253  32710  bnj1286  32712  bnj1280  32713  bnj1296  32714  bnj1311  32717  bnj1450  32743  bnj1498  32754  bnj1514  32756  bnj1501  32760  dfrdg2  33490  heibor1lem  35704  fnsnbt  39921  aomclem6  40587  ntrclsfv1  41342  ntrneifv1  41366  fnresdmss  42377  fnresfnco  44207  fnfocofob  44243  fnbrafvb  44318  uniimaprimaeqfv  44507  elsetpreimafvssdm  44511  imasetpreimafvbijlemfo  44530  fnxpdmdm  44995  plusfreseq  44999