Theorem fndm 6610

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5638  Fun wfun 6495   Fn wfn 6496

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 206  df-an 397  df-fn 6504

This theorem is referenced by:  fndmi  6611  fndmd  6612  funfni  6613  fndmu  6614  fnbr  6615  fncofn  6622  fnco  6623  fncoOLD  6624  fnresdm  6625  fnresdisj  6626  fnssresb  6628  fn0  6637  fnimadisj  6638  fnimaeq0  6639  fdmOLD  6683  f1dmOLD  6748  f1odm  6793  fvelimab  6919  fvun1  6937  eqfnfv2  6988  fndmdif  6997  fneqeql2  7002  elpreima  7013  fsn2  7087  fnprb  7163  fntpb  7164  fconst3  7168  fconst4  7169  fnfvima  7188  fnunirn  7206  dff13  7207  nvof1o  7231  f1eqcocnvOLD  7253  oprssov  7528  fnexALT  7888  dmmpogaOLD  8011  curry1  8041  curry1val  8042  curry2  8044  curry2val  8046  fparlem3  8051  fparlem4  8052  offsplitfpar  8056  suppvalfng  8104  suppvalfn  8105  suppfnss  8125  fnsuppres  8127  tposfo2  8185  frrlem3  8224  frrlem4  8225  wfrlem3OLD  8261  wfrlem4OLD  8263  wfrdmclOLD  8268  wfrlem12OLD  8271  smodm2  8306  smoel2  8314  tfrlem8  8335  tfrlem9  8336  tfrlem9a  8337  tfrlem13  8341  tz7.44-3  8359  rdglim  8377  frsucmptn  8390  oaabs2  8600  omabs  8602  ixpprc  8864  undifixp  8879  bren  8900  brenOLD  8901  fndmeng  8986  inf0  9566  r1lim  9717  jech9.3  9759  ssrankr1  9780  rankuni  9808  dfac3  10066  cfsmolem  10215  fin23lem31  10288  itunitc1  10365  ituniiun  10367  fnct  10482  cfpwsdom  10529  grur1  10765  genpdm  10947  fsuppmapnn0fiublem  13905  fsuppmapnn0fiub  13906  hashfn  14285  cshimadifsn  14730  cshimadifsn0  14731  shftfn  14970  rlimi2  15408  phimullem  16662  restsspw  17327  prdsdsval  17374  fnpr2ob  17454  sscpwex  17712  sscfn1  17714  sscfn2  17715  isssc  17717  funcres  17796  xpcbas  18080  xpchomfval  18081  gsumpropd2lem  18548  psgndmsubg  19298  dsmmbas2  21180  dsmmelbas  21182  islindf4  21281  restbas  22546  ptval  22958  kqcldsat  23121  kqnrmlem1  23131  kqnrmlem2  23132  hmphtop  23166  ustn0  23609  uniiccdif  24979  cpncn  25337  cpnres  25338  ulmf2  25780  tglngne  27555  uhgrn0  28081  upgrfn  28101  upgrex  28106  umgrfn  28113  fnunres1  31591  fcoinver  31592  nfpconfp  31613  mdetpmtr1  32493  coinflipspace  33169  bnj945  33474  bnj545  33596  bnj548  33598  bnj570  33606  bnj900  33630  bnj929  33637  bnj983  33652  bnj1018g  33664  bnj1018  33665  bnj1110  33683  bnj1145  33694  bnj1245  33715  bnj1253  33718  bnj1286  33720  bnj1280  33721  bnj1296  33722  bnj1311  33725  bnj1450  33751  bnj1498  33762  bnj1514  33764  bnj1501  33768  dfrdg2  34456  heibor1lem  36341  fnsnbt  40728  aomclem6  41444  tfsconcatun  41730  tfsconcatb0  41737  tfsconcat0i  41738  tfsconcat0b  41739  tfsconcatrev  41741  tfsnfin  41745  ntrclsfv1  42449  ntrneifv1  42473  fnresdmss  43507  dmmptif  43616  fnresfnco  45395  fnfocofob  45431  fnbrafvb  45506  uniimaprimaeqfv  45694  elsetpreimafvssdm  45698  imasetpreimafvbijlemfo  45717  fnxpdmdm  46182  plusfreseq  46186