Theorem fndm 6646

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5659  Fun wfun 6530   Fn wfn 6531

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 6539

This theorem is referenced by:  fndmi  6647  fndmd  6648  funfni  6649  fndmu  6650  fnbr  6651  fnunres1  6655  fncofn  6660  fnco  6661  fnresdm  6662  fnresdisj  6663  fnssresb  6665  fn0  6674  fnimadisj  6675  fnimaeq0  6676  f1odm  6827  fvelimab  6956  fvun1  6975  eqfnfv2  7027  fndmdif  7037  fneqeql2  7042  elpreima  7053  fsn2  7131  fnsnbg  7161  fnprb  7205  fntpb  7206  fconst3  7210  fconst4  7211  fnfvima  7230  ralima  7234  fnunirn  7251  dff13  7252  nvof1o  7278  oprssov  7581  fnexALT  7954  curry1  8108  curry1val  8109  curry2  8111  curry2val  8113  fparlem3  8118  fparlem4  8119  offsplitfpar  8123  suppvalfng  8171  suppvalfn  8172  suppfnss  8193  fnsuppres  8195  tposfo2  8253  frrlem3  8292  frrlem4  8293  wfrlem3OLD  8329  wfrlem4OLD  8331  wfrdmclOLD  8336  wfrlem12OLD  8339  smodm2  8374  smoel2  8382  tfrlem8  8403  tfrlem9  8404  tfrlem9a  8405  tfrlem13  8409  tz7.44-3  8427  rdglim  8445  frsucmptn  8458  oaabs2  8666  omabs  8668  ixpprc  8938  undifixp  8953  bren  8974  fndmeng  9054  inf0  9640  r1lim  9791  jech9.3  9833  ssrankr1  9854  rankuni  9882  dfac3  10140  cfsmolem  10289  fin23lem31  10362  itunitc1  10439  ituniiun  10441  fnct  10556  cfpwsdom  10603  grur1  10839  genpdm  11021  fsuppmapnn0fiublem  14013  fsuppmapnn0fiub  14014  hashfn  14398  cshimadifsn  14853  cshimadifsn0  14854  shftfn  15097  rlimi2  15535  phimullem  16803  restsspw  17450  prdsdsval  17497  fnpr2ob  17577  sscpwex  17833  sscfn1  17835  sscfn2  17836  isssc  17838  funcres  17914  xpcbas  18195  xpchomfval  18196  gsumpropd2lem  18662  psgndmsubg  19488  dsmmbas2  21702  dsmmelbas  21704  islindf4  21803  restbas  23101  ptval  23513  kqcldsat  23676  kqnrmlem1  23686  kqnrmlem2  23687  hmphtop  23721  ustn0  24164  uniiccdif  25536  cpncn  25895  cpnres  25896  ulmf2  26350  tglngne  28534  uhgrn0  29051  upgrfn  29071  upgrex  29076  umgrfn  29083  fcoinver  32590  nfpconfp  32615  opprabs  33502  mdetpmtr1  33859  coinflipspace  34518  bnj945  34809  bnj545  34931  bnj548  34933  bnj570  34941  bnj900  34965  bnj929  34972  bnj983  34987  bnj1018g  34999  bnj1018  35000  bnj1110  35018  bnj1145  35029  bnj1245  35050  bnj1253  35053  bnj1286  35055  bnj1280  35056  bnj1296  35057  bnj1311  35060  bnj1450  35086  bnj1498  35097  bnj1514  35099  bnj1501  35103  dfrdg2  35818  heibor1lem  37838  aks6d1c2lem4  42145  eqresfnbd  42250  aomclem6  43058  tfsconcatun  43336  tfsconcatb0  43343  tfsconcat0i  43344  tfsconcat0b  43345  tfsconcatrev  43347  tfsnfin  43351  ntrclsfv1  44054  ntrneifv1  44078  fnresdmss  45172  dmmptif  45270  fnresfnco  47050  fnfocofob  47088  fnbrafvb  47163  uniimaprimaeqfv  47376  elsetpreimafvssdm  47380  imasetpreimafvbijlemfo  47399  fnxpdmdm  48115  plusfreseq  48119  dmdm  49000