Theorem fndm 6603

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5631  Fun wfun 6493   Fn wfn 6494

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 6502

This theorem is referenced by:  fndmi  6604  fndmd  6605  funfni  6606  fndmu  6607  fnbr  6608  fnunres1  6612  fncofn  6617  fnco  6618  fnresdm  6619  fnresdisj  6620  fnssresb  6622  fn0  6631  fnimadisj  6632  fnimaeq0  6633  f1odm  6786  fvelimab  6915  fvun1  6934  eqfnfv2  6986  fndmdif  6996  fneqeql2  7001  elpreima  7012  fsn2  7090  fnsnbg  7120  fnprb  7164  fntpb  7165  fconst3  7169  fconst4  7170  fnfvima  7189  ralima  7193  fnunirn  7210  dff13  7211  nvof1o  7237  oprssov  7538  fnexALT  7909  curry1  8060  curry1val  8061  curry2  8063  curry2val  8065  fparlem3  8070  fparlem4  8071  offsplitfpar  8075  suppvalfng  8123  suppvalfn  8124  suppfnss  8145  fnsuppres  8147  tposfo2  8205  frrlem3  8244  frrlem4  8245  smodm2  8301  smoel2  8309  tfrlem8  8329  tfrlem9  8330  tfrlem9a  8331  tfrlem13  8335  tz7.44-3  8353  rdglim  8371  frsucmptn  8384  oaabs2  8590  omabs  8592  ixpprc  8869  undifixp  8884  bren  8905  fndmeng  8983  inf0  9550  r1lim  9701  jech9.3  9743  ssrankr1  9764  rankuni  9792  dfac3  10050  cfsmolem  10199  fin23lem31  10272  itunitc1  10349  ituniiun  10351  fnct  10466  cfpwsdom  10513  grur1  10749  genpdm  10931  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  hashfn  14316  cshimadifsn  14771  cshimadifsn0  14772  shftfn  15015  rlimi2  15456  phimullem  16725  restsspw  17370  prdsdsval  17417  fnpr2ob  17497  sscpwex  17753  sscfn1  17755  sscfn2  17756  isssc  17758  funcres  17834  xpcbas  18115  xpchomfval  18116  gsumpropd2lem  18582  psgndmsubg  19408  dsmmbas2  21622  dsmmelbas  21624  islindf4  21723  restbas  23021  ptval  23433  kqcldsat  23596  kqnrmlem1  23606  kqnrmlem2  23607  hmphtop  23641  ustn0  24084  uniiccdif  25455  cpncn  25814  cpnres  25815  ulmf2  26269  tglngne  28453  uhgrn0  28970  upgrfn  28990  upgrex  28995  umgrfn  29002  fcoinver  32506  nfpconfp  32529  opprabs  33426  mdetpmtr1  33786  coinflipspace  34445  bnj945  34736  bnj545  34858  bnj548  34860  bnj570  34868  bnj900  34892  bnj929  34899  bnj983  34914  bnj1018g  34926  bnj1018  34927  bnj1110  34945  bnj1145  34956  bnj1245  34977  bnj1253  34980  bnj1286  34982  bnj1280  34983  bnj1296  34984  bnj1311  34987  bnj1450  35013  bnj1498  35024  bnj1514  35026  bnj1501  35030  dfrdg2  35756  heibor1lem  37776  aks6d1c2lem4  42088  eqresfnbd  42193  aomclem6  43021  tfsconcatun  43299  tfsconcatb0  43306  tfsconcat0i  43307  tfsconcat0b  43308  tfsconcatrev  43310  tfsnfin  43314  ntrclsfv1  44017  ntrneifv1  44041  fnresdmss  45135  dmmptif  45233  fnresfnco  47015  fnfocofob  47053  fnbrafvb  47128  uniimaprimaeqfv  47356  elsetpreimafvssdm  47360  imasetpreimafvbijlemfo  47379  fnxpdmdm  48121  plusfreseq  48125  dmdm  49015