Theorem fndm 6624

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

Syntax hints:   → wi 4   = wceq 1560  dom cdm 5647  Fun wfun 6515   Fn wfn 6516

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 209  df-an 400  df-fn 6524

This theorem is referenced by:  fndmi  6625  fndmd  6626  funfni  6627  fndmu  6628  fnbr  6629  fnunres1  6633  fncofn  6638  fnco  6639  fnresdm  6640  fnresdisj  6641  fnssresb  6643  fn0  6652  fnimadisj  6653  fnimaeq0  6654  f1odmOLD  6811  fvelimab  6939  fvun1  6958  eqfnfv2  7012  fndmdif  7023  fneqeql2  7028  elpreima  7039  fsn2  7118  fnsnbg  7148  fnprb  7192  fntpb  7193  fconst3  7197  fconst4  7198  fnfvima  7217  ralima  7221  fnunirn  7237  dff13  7238  nvof1o  7264  oprssov  7565  fnexALT  7932  curry1  8083  curry1val  8084  curry2  8086  curry2val  8088  fparlem3  8093  fparlem4  8094  offsplitfpar  8098  suppvalfng  8147  suppvalfn  8148  suppfnss  8169  fnsuppres  8171  tposfo2  8229  frrlem3  8269  frrlem4  8270  smodm2  8326  smoel2  8334  tfrlem8  8355  tfrlem9  8356  tfrlem9a  8357  tfrlem13  8361  tz7.44-3  8379  rdglim  8397  frsucmptn  8410  oaabs2  8619  omabs  8621  ixpprc  8901  undifixp  8916  bren  8937  fndmeng  9016  tfsnfin2  9306  inf0  9576  r1lim  9730  jech9.3  9772  ssrankr1  9793  rankuni  9821  dfac3  10077  cfsmolem  10227  fin23lem31  10300  itunitc1  10377  ituniiun  10379  fnct  10494  cfpwsdom  10542  grur1  10778  genpdm  10960  fsuppmapnn0fiublem  14003  fsuppmapnn0fiub  14004  hashfn  14388  cshimadifsn  14842  cshimadifsn0  14843  shftfn  15086  rlimi2  15541  phimullem  16814  restsspw  17460  prdsdsval  17507  fnpr2ob  17588  sscpwex  17848  sscfn1  17850  sscfn2  17851  isssc  17853  funcres  17929  xpcbas  18210  xpchomfval  18211  gsumpropd2lem  18713  psgndmsubg  19542  dsmmbas2  21786  dsmmelbas  21788  islindf4  21887  restbas  23215  ptval  23627  kqcldsat  23790  kqnrmlem1  23800  kqnrmlem2  23801  hmphtop  23835  ustn0  24278  uniiccdif  25637  cpncn  25995  cpnres  25996  ulmf2  26444  tglngne  28716  uhgrn0  29265  upgrfn  29285  upgrex  29290  umgrfn  29297  fcoinver  32801  fresunsn  32824  nfpconfp  32831  opprabs  33667  mdetpmtr1  34117  coinflipspace  34775  bnj945  35066  bnj545  35187  bnj548  35189  bnj570  35197  bnj900  35221  bnj929  35228  bnj983  35243  bnj1018g  35255  bnj1018  35256  bnj1110  35274  bnj1145  35285  bnj1245  35306  bnj1253  35309  bnj1286  35311  bnj1280  35312  bnj1296  35313  bnj1311  35316  bnj1450  35342  bnj1498  35353  bnj1514  35355  bnj1501  35359  dfrdg2  36140  heibor1lem  38305  aks6d1c2lem4  42741  eqresfnbd  42848  aomclem6  43633  tfsconcatun  43911  tfsconcatb0  43918  tfsconcat0i  43919  tfsconcat0b  43920  tfsconcatrev  43922  tfsnfin  43926  ntrclsfv1  44628  ntrneifv1  44652  fnresdmss  45743  dmmptif  45838  fnresfnco  47632  fnfocofob  47670  fnbrafvb  47745  uniimaprimaeqfv  47985  elsetpreimafvssdm  47989  imasetpreimafvbijlemfo  48008  fnxpdmdm  48779  plusfreseq  48783  dmdm  49671