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  17757  sscfn1  17759  sscfn2  17760  isssc  17762  funcres  17838  xpcbas  18119  xpchomfval  18120  gsumpropd2lem  18588  psgndmsubg  19416  dsmmbas2  21679  dsmmelbas  21681  islindf4  21780  restbas  23078  ptval  23490  kqcldsat  23653  kqnrmlem1  23663  kqnrmlem2  23664  hmphtop  23698  ustn0  24141  uniiccdif  25512  cpncn  25871  cpnres  25872  ulmf2  26326  tglngne  28530  uhgrn0  29047  upgrfn  29067  upgrex  29072  umgrfn  29079  fcoinver  32583  nfpconfp  32606  opprabs  33446  mdetpmtr1  33806  coinflipspace  34465  bnj945  34756  bnj545  34878  bnj548  34880  bnj570  34888  bnj900  34912  bnj929  34919  bnj983  34934  bnj1018g  34946  bnj1018  34947  bnj1110  34965  bnj1145  34976  bnj1245  34997  bnj1253  35000  bnj1286  35002  bnj1280  35003  bnj1296  35004  bnj1311  35007  bnj1450  35033  bnj1498  35044  bnj1514  35046  bnj1501  35050  dfrdg2  35776  heibor1lem  37796  aks6d1c2lem4  42108  eqresfnbd  42213  aomclem6  43041  tfsconcatun  43319  tfsconcatb0  43326  tfsconcat0i  43327  tfsconcat0b  43328  tfsconcatrev  43330  tfsnfin  43334  ntrclsfv1  44037  ntrneifv1  44061  fnresdmss  45155  dmmptif  45253  fnresfnco  47035  fnfocofob  47073  fnbrafvb  47148  uniimaprimaeqfv  47376  elsetpreimafvssdm  47380  imasetpreimafvbijlemfo  47399  fnxpdmdm  48141  plusfreseq  48145  dmdm  49035