Theorem fndm 6520

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580  Fun wfun 6412   Fn wfn 6413

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 396  df-fn 6421

This theorem is referenced by:  fndmi  6521  fndmd  6522  funfni  6523  fndmu  6524  fnbr  6525  fncofn  6532  fnco  6533  fncoOLD  6534  fnresdm  6535  fnresdisj  6536  fnssresb  6538  fn0  6548  fnimadisj  6549  fnimaeq0  6550  fdmOLD  6594  f1dmOLD  6659  f1odm  6704  fvelimab  6823  fvun1  6841  eqfnfv2  6892  fndmdif  6901  fneqeql2  6906  elpreima  6917  fsn2  6990  fnprb  7066  fntpb  7067  fconst3  7071  fconst4  7072  fnfvima  7091  fnunirn  7108  dff13  7109  nvof1o  7133  f1eqcocnvOLD  7154  oprssov  7419  fnexALT  7767  dmmpogaOLD  7887  curry1  7915  curry1val  7916  curry2  7918  curry2val  7920  fparlem3  7925  fparlem4  7926  offsplitfpar  7931  suppvalfng  7955  suppvalfn  7956  suppfnss  7976  fnsuppres  7978  tposfo2  8036  frrlem3  8075  frrlem4  8076  wfrlem3OLD  8112  wfrlem4OLD  8114  wfrdmclOLD  8119  wfrlem12OLD  8122  smodm2  8157  smoel2  8165  tfrlem8  8186  tfrlem9  8187  tfrlem9a  8188  tfrlem13  8192  tz7.44-3  8210  rdglim  8228  frsucmptn  8240  oaabs2  8439  omabs  8441  ixpprc  8665  undifixp  8680  bren  8701  brenOLD  8702  fndmeng  8779  inf0  9309  r1lim  9461  jech9.3  9503  ssrankr1  9524  rankuni  9552  dfac3  9808  cfsmolem  9957  fin23lem31  10030  itunitc1  10107  ituniiun  10109  fnct  10224  cfpwsdom  10271  grur1  10507  genpdm  10689  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  hashfn  14018  cshimadifsn  14470  cshimadifsn0  14471  shftfn  14712  rlimi2  15151  phimullem  16408  restsspw  17059  prdsdsval  17106  fnpr2ob  17186  sscpwex  17444  sscfn1  17446  sscfn2  17447  isssc  17449  funcres  17527  xpcbas  17811  xpchomfval  17812  gsumpropd2lem  18278  psgndmsubg  19025  dsmmbas2  20854  dsmmelbas  20856  islindf4  20955  restbas  22217  ptval  22629  kqcldsat  22792  kqnrmlem1  22802  kqnrmlem2  22803  hmphtop  22837  ustn0  23280  uniiccdif  24647  cpncn  25005  cpnres  25006  ulmf2  25448  tglngne  26815  uhgrn0  27340  upgrfn  27360  upgrex  27365  umgrfn  27372  fnunres1  30846  fcoinver  30847  nfpconfp  30868  mdetpmtr1  31675  coinflipspace  32347  bnj945  32653  bnj545  32775  bnj548  32777  bnj570  32785  bnj900  32809  bnj929  32816  bnj983  32831  bnj1018g  32843  bnj1018  32844  bnj1110  32862  bnj1145  32873  bnj1245  32894  bnj1253  32897  bnj1286  32899  bnj1280  32900  bnj1296  32901  bnj1311  32904  bnj1450  32930  bnj1498  32941  bnj1514  32943  bnj1501  32947  dfrdg2  33677  heibor1lem  35894  fnsnbt  40134  aomclem6  40800  ntrclsfv1  41554  ntrneifv1  41578  fnresdmss  42593  fnresfnco  44422  fnfocofob  44458  fnbrafvb  44533  uniimaprimaeqfv  44722  elsetpreimafvssdm  44726  imasetpreimafvbijlemfo  44745  fnxpdmdm  45210  plusfreseq  45214