Theorem fndm 6585

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5619  Fun wfun 6476   Fn wfn 6477

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 6485

This theorem is referenced by:  fndmi  6586  fndmd  6587  funfni  6588  fndmu  6589  fnbr  6590  fnunres1  6594  fncofn  6599  fnco  6600  fnresdm  6601  fnresdisj  6602  fnssresb  6604  fn0  6613  fnimadisj  6614  fnimaeq0  6615  f1odm  6768  fvelimab  6895  fvun1  6914  eqfnfv2  6966  fndmdif  6976  fneqeql2  6981  elpreima  6992  fsn2  7070  fnsnbg  7100  fnprb  7144  fntpb  7145  fconst3  7149  fconst4  7150  fnfvima  7169  ralima  7173  fnunirn  7190  dff13  7191  nvof1o  7217  oprssov  7518  fnexALT  7886  curry1  8037  curry1val  8038  curry2  8040  curry2val  8042  fparlem3  8047  fparlem4  8048  offsplitfpar  8052  suppvalfng  8100  suppvalfn  8101  suppfnss  8122  fnsuppres  8124  tposfo2  8182  frrlem3  8221  frrlem4  8222  smodm2  8278  smoel2  8286  tfrlem8  8306  tfrlem9  8307  tfrlem9a  8308  tfrlem13  8312  tz7.44-3  8330  rdglim  8348  frsucmptn  8361  oaabs2  8567  omabs  8569  ixpprc  8846  undifixp  8861  bren  8882  fndmeng  8960  inf0  9517  r1lim  9668  jech9.3  9710  ssrankr1  9731  rankuni  9759  dfac3  10015  cfsmolem  10164  fin23lem31  10237  itunitc1  10314  ituniiun  10316  fnct  10431  cfpwsdom  10478  grur1  10714  genpdm  10896  fsuppmapnn0fiublem  13897  fsuppmapnn0fiub  13898  hashfn  14282  cshimadifsn  14736  cshimadifsn0  14737  shftfn  14980  rlimi2  15421  phimullem  16690  restsspw  17335  prdsdsval  17382  fnpr2ob  17462  sscpwex  17722  sscfn1  17724  sscfn2  17725  isssc  17727  funcres  17803  xpcbas  18084  xpchomfval  18085  gsumpropd2lem  18553  psgndmsubg  19381  dsmmbas2  21644  dsmmelbas  21646  islindf4  21745  restbas  23043  ptval  23455  kqcldsat  23618  kqnrmlem1  23628  kqnrmlem2  23629  hmphtop  23663  ustn0  24106  uniiccdif  25477  cpncn  25836  cpnres  25837  ulmf2  26291  tglngne  28495  uhgrn0  29012  upgrfn  29032  upgrex  29037  umgrfn  29044  fcoinver  32548  nfpconfp  32575  opprabs  33419  mdetpmtr1  33790  coinflipspace  34449  bnj945  34740  bnj545  34862  bnj548  34864  bnj570  34872  bnj900  34896  bnj929  34903  bnj983  34918  bnj1018g  34930  bnj1018  34931  bnj1110  34949  bnj1145  34960  bnj1245  34981  bnj1253  34984  bnj1286  34986  bnj1280  34987  bnj1296  34988  bnj1311  34991  bnj1450  35017  bnj1498  35028  bnj1514  35030  bnj1501  35034  dfrdg2  35769  heibor1lem  37789  aks6d1c2lem4  42100  eqresfnbd  42205  aomclem6  43032  tfsconcatun  43310  tfsconcatb0  43317  tfsconcat0i  43318  tfsconcat0b  43319  tfsconcatrev  43321  tfsnfin  43325  ntrclsfv1  44028  ntrneifv1  44052  fnresdmss  45146  dmmptif  45244  fnresfnco  47025  fnfocofob  47063  fnbrafvb  47138  uniimaprimaeqfv  47366  elsetpreimafvssdm  47370  imasetpreimafvbijlemfo  47389  fnxpdmdm  48144  plusfreseq  48148  dmdm  49038