Theorem fndm 6653

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677  Fun wfun 6538   Fn wfn 6539

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 398  df-fn 6547

This theorem is referenced by:  fndmi  6654  fndmd  6655  funfni  6656  fndmu  6657  fnbr  6658  fnunres1  6662  fncofn  6667  fnco  6668  fncoOLD  6669  fnresdm  6670  fnresdisj  6671  fnssresb  6673  fn0  6682  fnimadisj  6683  fnimaeq0  6684  fdmOLD  6728  f1dmOLD  6793  f1odm  6838  fvelimab  6965  fvun1  6983  eqfnfv2  7034  fndmdif  7044  fneqeql2  7049  elpreima  7060  fsn2  7134  fnprb  7210  fntpb  7211  fconst3  7215  fconst4  7216  fnfvima  7235  fnunirn  7253  dff13  7254  nvof1o  7278  f1eqcocnvOLD  7300  oprssov  7576  fnexALT  7937  dmmpogaOLD  8060  curry1  8090  curry1val  8091  curry2  8093  curry2val  8095  fparlem3  8100  fparlem4  8101  offsplitfpar  8105  suppvalfng  8153  suppvalfn  8154  suppfnss  8174  fnsuppres  8176  tposfo2  8234  frrlem3  8273  frrlem4  8274  wfrlem3OLD  8310  wfrlem4OLD  8312  wfrdmclOLD  8317  wfrlem12OLD  8320  smodm2  8355  smoel2  8363  tfrlem8  8384  tfrlem9  8385  tfrlem9a  8386  tfrlem13  8390  tz7.44-3  8408  rdglim  8426  frsucmptn  8439  oaabs2  8648  omabs  8650  ixpprc  8913  undifixp  8928  bren  8949  brenOLD  8950  fndmeng  9035  inf0  9616  r1lim  9767  jech9.3  9809  ssrankr1  9830  rankuni  9858  dfac3  10116  cfsmolem  10265  fin23lem31  10338  itunitc1  10415  ituniiun  10417  fnct  10532  cfpwsdom  10579  grur1  10815  genpdm  10997  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  hashfn  14335  cshimadifsn  14780  cshimadifsn0  14781  shftfn  15020  rlimi2  15458  phimullem  16712  restsspw  17377  prdsdsval  17424  fnpr2ob  17504  sscpwex  17762  sscfn1  17764  sscfn2  17765  isssc  17767  funcres  17846  xpcbas  18130  xpchomfval  18131  gsumpropd2lem  18598  psgndmsubg  19370  dsmmbas2  21292  dsmmelbas  21294  islindf4  21393  restbas  22662  ptval  23074  kqcldsat  23237  kqnrmlem1  23247  kqnrmlem2  23248  hmphtop  23282  ustn0  23725  uniiccdif  25095  cpncn  25453  cpnres  25454  ulmf2  25896  tglngne  27801  uhgrn0  28327  upgrfn  28347  upgrex  28352  umgrfn  28359  fcoinver  31835  nfpconfp  31856  opprabs  32596  mdetpmtr1  32803  coinflipspace  33479  bnj945  33784  bnj545  33906  bnj548  33908  bnj570  33916  bnj900  33940  bnj929  33947  bnj983  33962  bnj1018g  33974  bnj1018  33975  bnj1110  33993  bnj1145  34004  bnj1245  34025  bnj1253  34028  bnj1286  34030  bnj1280  34031  bnj1296  34032  bnj1311  34035  bnj1450  34061  bnj1498  34072  bnj1514  34074  bnj1501  34078  dfrdg2  34767  heibor1lem  36677  fnsnbt  41051  eqresfnbd  41054  aomclem6  41801  tfsconcatun  42087  tfsconcatb0  42094  tfsconcat0i  42095  tfsconcat0b  42096  tfsconcatrev  42098  tfsnfin  42102  ntrclsfv1  42806  ntrneifv1  42830  fnresdmss  43864  dmmptif  43971  fnresfnco  45751  fnfocofob  45787  fnbrafvb  45862  uniimaprimaeqfv  46050  elsetpreimafvssdm  46054  imasetpreimafvbijlemfo  46073  fnxpdmdm  46538  plusfreseq  46542