Theorem fndm 6639

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

Syntax hints:   → wi 4   = wceq 1567  dom cdm 5662  Fun wfun 6531   Fn wfn 6532

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 6540

This theorem is referenced by:  fndmi  6640  fndmd  6641  funfni  6642  fndmu  6643  fnbr  6644  fnunres1  6648  fncofn  6653  fnco  6654  fnresdm  6655  fnresdisj  6656  fnssresb  6658  fn0  6667  fnimadisj  6668  fnimaeq0  6669  f1odmOLD  6826  fvelimab  6954  fvun1  6973  eqfnfv2  7027  fndmdif  7038  fneqeql2  7043  elpreima  7054  fsn2  7133  fnsnbg  7163  fnprb  7207  fntpb  7208  fconst3  7212  fconst4  7213  fnfvima  7232  ralima  7236  fnunirn  7252  dff13  7253  nvof1o  7279  oprssov  7580  fnexALT  7947  curry1  8098  curry1val  8099  curry2  8101  curry2val  8103  fparlem3  8108  fparlem4  8109  offsplitfpar  8113  suppvalfng  8162  suppvalfn  8163  suppfnss  8184  fnsuppres  8186  tposfo2  8244  frrlem3  8284  frrlem4  8285  smodm2  8341  smoel2  8349  tfrlem8  8370  tfrlem9  8371  tfrlem9a  8372  tfrlem13  8376  tz7.44-3  8394  rdglim  8412  frsucmptn  8425  oaabs2  8634  omabs  8636  ixpprc  8916  undifixp  8931  bren  8952  fndmeng  9031  tfsnfin2  9319  inf0  9589  r1lim  9743  jech9.3  9785  ssrankr1  9806  rankuni  9834  dfac3  10104  cfsmolem  10253  fin23lem31  10326  itunitc1  10403  ituniiun  10405  fnct  10520  cfpwsdom  10568  grur1  10804  genpdm  10986  fsuppmapnn0fiublem  14025  fsuppmapnn0fiub  14026  hashfn  14410  cshimadifsn  14865  cshimadifsn0  14866  shftfn  15109  rlimi2  15564  phimullem  16837  restsspw  17483  prdsdsval  17530  fnpr2ob  17611  sscpwex  17871  sscfn1  17873  sscfn2  17874  isssc  17876  funcres  17952  xpcbas  18233  xpchomfval  18234  gsumpropd2lem  18736  psgndmsubg  19571  dsmmbas2  21855  dsmmelbas  21857  islindf4  21956  restbas  23283  ptval  23695  kqcldsat  23858  kqnrmlem1  23868  kqnrmlem2  23869  hmphtop  23903  ustn0  24346  uniiccdif  25705  cpncn  26063  cpnres  26064  ulmf2  26512  tglngne  28784  uhgrn0  29357  upgrfn  29377  upgrex  29382  umgrfn  29389  fcoinver  32889  fresunsn  32910  nfpconfp  32917  opprabs  33708  mdetpmtr1  34157  coinflipspace  34815  bnj945  35106  bnj545  35227  bnj548  35229  bnj570  35237  bnj900  35261  bnj929  35268  bnj983  35283  bnj1018g  35295  bnj1018  35296  bnj1110  35314  bnj1145  35325  bnj1245  35346  bnj1253  35349  bnj1286  35351  bnj1280  35352  bnj1296  35353  bnj1311  35356  bnj1450  35382  bnj1498  35393  bnj1514  35395  bnj1501  35399  dfrdg2  36183  heibor1lem  38347  aks6d1c2lem4  42783  eqresfnbd  42892  aomclem6  43677  tfsconcatun  43955  tfsconcatb0  43962  tfsconcat0i  43963  tfsconcat0b  43964  tfsconcatrev  43966  tfsnfin  43970  ntrclsfv1  44672  ntrneifv1  44696  fnresdmss  45777  dmmptif  45872  fnresfnco  47666  fnfocofob  47704  fnbrafvb  47779  uniimaprimaeqfv  48019  elsetpreimafvssdm  48023  imasetpreimafvbijlemfo  48042  fnxpdmdm  48813  plusfreseq  48817  dmdm  49715