Theorem fndm 6638

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 502	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1570  dom cdm 5661  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 210  df-an 401  df-fn 6539

This theorem is referenced by:  fndmi  6639  fndmd  6640  funfni  6641  fndmu  6642  fnbr  6643  fnunres1  6647  fncofn  6652  fnco  6653  fnresdm  6654  fnresdisj  6655  fnssresb  6657  fn0  6666  fnimadisj  6667  fnimaeq0  6668  f1odmOLD  6825  fvelimab  6953  fvun1  6972  eqfnfv2  7026  fndmdif  7037  fneqeql2  7042  elpreima  7053  fsn2  7132  fnsnbg  7162  fnprb  7206  fntpb  7207  fconst3  7211  fconst4  7212  fnfvima  7231  ralima  7235  fnunirn  7251  dff13  7252  nvof1o  7278  oprssov  7579  fnexALT  7944  curry1  8095  curry1val  8096  curry2  8098  curry2val  8100  fparlem3  8105  fparlem4  8106  offsplitfpar  8110  suppvalfng  8159  suppvalfn  8160  suppfnss  8181  fnsuppres  8183  tposfo2  8241  frrlem3  8281  frrlem4  8282  smodm2  8338  smoel2  8346  tfrlem8  8367  tfrlem9  8368  tfrlem9a  8369  tfrlem13  8373  tz7.44-3  8391  rdglim  8409  frsucmptn  8422  oaabs2  8631  omabs  8633  ixpprc  8913  undifixp  8928  bren  8949  fndmeng  9028  tfsnfin2  9316  inf0  9586  r1lim  9740  jech9.3  9782  ssrankr1  9803  rankuni  9831  dfac3  10101  cfsmolem  10249  fin23lem31  10322  itunitc1  10399  ituniiun  10401  fnct  10516  cfpwsdom  10564  grur1  10800  genpdm  10982  fsuppmapnn0fiublem  14022  fsuppmapnn0fiub  14023  hashfn  14407  cshimadifsn  14862  cshimadifsn0  14863  shftfn  15106  rlimi2  15561  phimullem  16833  restsspw  17479  prdsdsval  17526  fnpr2ob  17607  sscpwex  17867  sscfn1  17869  sscfn2  17870  isssc  17872  funcres  17948  xpcbas  18229  xpchomfval  18230  gsumpropd2lem  18732  psgndmsubg  19567  dsmmbas2  21887  dsmmelbas  21889  islindf4  21988  restbas  23315  ptval  23727  kqcldsat  23890  kqnrmlem1  23900  kqnrmlem2  23901  hmphtop  23935  ustn0  24378  uniiccdif  25737  cpncn  26095  cpnres  26096  ulmf2  26547  tglngne  28819  uhgrn0  29417  upgrfn  29437  upgrex  29442  umgrfn  29449  fcoinver  32949  fresunsn  32970  nfpconfp  32977  opprabs  33764  mdetpmtr1  34213  coinflipspace  34871  bnj945  35162  bnj545  35283  bnj548  35285  bnj570  35293  bnj900  35317  bnj929  35324  bnj983  35339  bnj1018g  35351  bnj1018  35352  bnj1110  35370  bnj1145  35381  bnj1245  35402  bnj1253  35405  bnj1286  35407  bnj1280  35408  bnj1296  35409  bnj1311  35412  bnj1450  35438  bnj1498  35449  bnj1514  35451  bnj1501  35455  dfrdg2  36285  heibor1lem  38460  aks6d1c2lem4  42894  eqresfnbd  43003  aomclem6  43786  tfsconcatun  44064  tfsconcatb0  44071  tfsconcat0i  44072  tfsconcat0b  44073  tfsconcatrev  44075  tfsnfin  44079  ntrclsfv1  44781  ntrneifv1  44805  fnresdmss  45886  dmmptif  45981  fnresfnco  47778  fnfocofob  47816  fnbrafvb  47891  uniimaprimaeqfv  48131  elsetpreimafvssdm  48135  imasetpreimafvbijlemfo  48154  fnxpdmdm  48925  plusfreseq  48929  dmdm  49831