Theorem fndm 6595

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5624  Fun wfun 6486   Fn wfn 6487

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 6495

This theorem is referenced by:  fndmi  6596  fndmd  6597  funfni  6598  fndmu  6599  fnbr  6600  fnunres1  6604  fncofn  6609  fnco  6610  fnresdm  6611  fnresdisj  6612  fnssresb  6614  fn0  6623  fnimadisj  6624  fnimaeq0  6625  f1odm  6778  fvelimab  6906  fvun1  6925  eqfnfv2  6977  fndmdif  6987  fneqeql2  6992  elpreima  7003  fsn2  7081  fnsnbg  7110  fnprb  7154  fntpb  7155  fconst3  7159  fconst4  7160  fnfvima  7179  ralima  7183  fnunirn  7199  dff13  7200  nvof1o  7226  oprssov  7527  fnexALT  7895  curry1  8046  curry1val  8047  curry2  8049  curry2val  8051  fparlem3  8056  fparlem4  8057  offsplitfpar  8061  suppvalfng  8109  suppvalfn  8110  suppfnss  8131  fnsuppres  8133  tposfo2  8191  frrlem3  8230  frrlem4  8231  smodm2  8287  smoel2  8295  tfrlem8  8315  tfrlem9  8316  tfrlem9a  8317  tfrlem13  8321  tz7.44-3  8339  rdglim  8357  frsucmptn  8370  oaabs2  8577  omabs  8579  ixpprc  8857  undifixp  8872  bren  8893  fndmeng  8972  tfsnfin2  9263  inf0  9530  r1lim  9684  jech9.3  9726  ssrankr1  9747  rankuni  9775  dfac3  10031  cfsmolem  10180  fin23lem31  10253  itunitc1  10330  ituniiun  10332  fnct  10447  cfpwsdom  10495  grur1  10731  genpdm  10913  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  hashfn  14298  cshimadifsn  14752  cshimadifsn0  14753  shftfn  14996  rlimi2  15437  phimullem  16706  restsspw  17351  prdsdsval  17398  fnpr2ob  17479  sscpwex  17739  sscfn1  17741  sscfn2  17742  isssc  17744  funcres  17820  xpcbas  18101  xpchomfval  18102  gsumpropd2lem  18604  psgndmsubg  19431  dsmmbas2  21692  dsmmelbas  21694  islindf4  21793  restbas  23102  ptval  23514  kqcldsat  23677  kqnrmlem1  23687  kqnrmlem2  23688  hmphtop  23722  ustn0  24165  uniiccdif  25535  cpncn  25894  cpnres  25895  ulmf2  26349  tglngne  28622  uhgrn0  29140  upgrfn  29160  upgrex  29165  umgrfn  29172  fcoinver  32679  fresunsn  32703  nfpconfp  32710  opprabs  33563  mdetpmtr1  33980  coinflipspace  34638  bnj945  34929  bnj545  35051  bnj548  35053  bnj570  35061  bnj900  35085  bnj929  35092  bnj983  35107  bnj1018g  35119  bnj1018  35120  bnj1110  35138  bnj1145  35149  bnj1245  35170  bnj1253  35173  bnj1286  35175  bnj1280  35176  bnj1296  35177  bnj1311  35180  bnj1450  35206  bnj1498  35217  bnj1514  35219  bnj1501  35223  dfrdg2  35987  heibor1lem  38010  aks6d1c2lem4  42381  eqresfnbd  42488  aomclem6  43301  tfsconcatun  43579  tfsconcatb0  43586  tfsconcat0i  43587  tfsconcat0b  43588  tfsconcatrev  43590  tfsnfin  43594  ntrclsfv1  44296  ntrneifv1  44320  fnresdmss  45412  dmmptif  45510  fnresfnco  47287  fnfocofob  47325  fnbrafvb  47400  uniimaprimaeqfv  47628  elsetpreimafvssdm  47632  imasetpreimafvbijlemfo  47651  fnxpdmdm  48406  plusfreseq  48410  dmdm  49298