Theorem fndm 6642

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5666  Fun wfun 6527   Fn wfn 6528

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 396  df-fn 6536

This theorem is referenced by:  fndmi  6643  fndmd  6644  funfni  6645  fndmu  6646  fnbr  6647  fnunres1  6651  fncofn  6656  fnco  6657  fncoOLD  6658  fnresdm  6659  fnresdisj  6660  fnssresb  6662  fn0  6671  fnimadisj  6672  fnimaeq0  6673  fdmOLD  6717  f1dmOLD  6782  f1odm  6827  fvelimab  6954  fvun1  6972  eqfnfv2  7023  fndmdif  7033  fneqeql2  7038  elpreima  7049  fsn2  7126  fnprb  7201  fntpb  7202  fconst3  7206  fconst4  7207  fnfvima  7226  fnunirn  7245  dff13  7246  nvof1o  7270  f1eqcocnvOLD  7292  oprssov  7569  fnexALT  7930  dmmpogaOLD  8053  curry1  8084  curry1val  8085  curry2  8087  curry2val  8089  fparlem3  8094  fparlem4  8095  offsplitfpar  8099  suppvalfng  8147  suppvalfn  8148  suppfnss  8168  fnsuppres  8170  tposfo2  8229  frrlem3  8268  frrlem4  8269  wfrlem3OLD  8305  wfrlem4OLD  8307  wfrdmclOLD  8312  wfrlem12OLD  8315  smodm2  8350  smoel2  8358  tfrlem8  8379  tfrlem9  8380  tfrlem9a  8381  tfrlem13  8385  tz7.44-3  8403  rdglim  8421  frsucmptn  8434  oaabs2  8644  omabs  8646  ixpprc  8909  undifixp  8924  bren  8945  brenOLD  8946  fndmeng  9031  inf0  9612  r1lim  9763  jech9.3  9805  ssrankr1  9826  rankuni  9854  dfac3  10112  cfsmolem  10261  fin23lem31  10334  itunitc1  10411  ituniiun  10413  fnct  10528  cfpwsdom  10575  grur1  10811  genpdm  10993  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  hashfn  14332  cshimadifsn  14777  cshimadifsn0  14778  shftfn  15017  rlimi2  15455  phimullem  16711  restsspw  17376  prdsdsval  17423  fnpr2ob  17503  sscpwex  17761  sscfn1  17763  sscfn2  17764  isssc  17766  funcres  17845  xpcbas  18132  xpchomfval  18133  gsumpropd2lem  18602  psgndmsubg  19412  dsmmbas2  21600  dsmmelbas  21602  islindf4  21701  restbas  22984  ptval  23396  kqcldsat  23559  kqnrmlem1  23569  kqnrmlem2  23570  hmphtop  23604  ustn0  24047  uniiccdif  25429  cpncn  25788  cpnres  25789  ulmf2  26237  tglngne  28270  uhgrn0  28796  upgrfn  28816  upgrex  28821  umgrfn  28828  fcoinver  32304  nfpconfp  32325  opprabs  33065  mdetpmtr1  33292  coinflipspace  33968  bnj945  34273  bnj545  34395  bnj548  34397  bnj570  34405  bnj900  34429  bnj929  34436  bnj983  34451  bnj1018g  34463  bnj1018  34464  bnj1110  34482  bnj1145  34493  bnj1245  34514  bnj1253  34517  bnj1286  34519  bnj1280  34520  bnj1296  34521  bnj1311  34524  bnj1450  34550  bnj1498  34561  bnj1514  34563  bnj1501  34567  dfrdg2  35262  heibor1lem  37167  fnsnbt  41544  eqresfnbd  41547  aomclem6  42290  tfsconcatun  42576  tfsconcatb0  42583  tfsconcat0i  42584  tfsconcat0b  42585  tfsconcatrev  42587  tfsnfin  42591  ntrclsfv1  43295  ntrneifv1  43319  fnresdmss  44352  dmmptif  44456  fnresfnco  46236  fnfocofob  46272  fnbrafvb  46347  uniimaprimaeqfv  46535  elsetpreimafvssdm  46539  imasetpreimafvbijlemfo  46558  fnxpdmdm  47023  plusfreseq  47027