Theorem fndm 6652

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5667  Fun wfun 6536   Fn wfn 6537

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 6545

This theorem is referenced by:  fndmi  6653  fndmd  6654  funfni  6655  fndmu  6656  fnbr  6657  fnunres1  6661  fncofn  6666  fnco  6667  fnresdm  6668  fnresdisj  6669  fnssresb  6671  fn0  6680  fnimadisj  6681  fnimaeq0  6682  f1odm  6833  fvelimab  6962  fvun1  6981  eqfnfv2  7033  fndmdif  7043  fneqeql2  7048  elpreima  7059  fsn2  7137  fnsnbg  7167  fnprb  7211  fntpb  7212  fconst3  7216  fconst4  7217  fnfvima  7236  ralima  7240  fnunirn  7257  dff13  7258  nvof1o  7283  oprssov  7585  fnexALT  7958  curry1  8112  curry1val  8113  curry2  8115  curry2val  8117  fparlem3  8122  fparlem4  8123  offsplitfpar  8127  suppvalfng  8175  suppvalfn  8176  suppfnss  8197  fnsuppres  8199  tposfo2  8257  frrlem3  8296  frrlem4  8297  wfrlem3OLD  8333  wfrlem4OLD  8335  wfrdmclOLD  8340  wfrlem12OLD  8343  smodm2  8378  smoel2  8386  tfrlem8  8407  tfrlem9  8408  tfrlem9a  8409  tfrlem13  8413  tz7.44-3  8431  rdglim  8449  frsucmptn  8462  oaabs2  8670  omabs  8672  ixpprc  8942  undifixp  8957  bren  8978  fndmeng  9058  inf0  9644  r1lim  9795  jech9.3  9837  ssrankr1  9858  rankuni  9886  dfac3  10144  cfsmolem  10293  fin23lem31  10366  itunitc1  10443  ituniiun  10445  fnct  10560  cfpwsdom  10607  grur1  10843  genpdm  11025  fsuppmapnn0fiublem  14014  fsuppmapnn0fiub  14015  hashfn  14397  cshimadifsn  14851  cshimadifsn0  14852  shftfn  15095  rlimi2  15533  phimullem  16799  restsspw  17452  prdsdsval  17499  fnpr2ob  17579  sscpwex  17835  sscfn1  17837  sscfn2  17838  isssc  17840  funcres  17917  xpcbas  18198  xpchomfval  18199  gsumpropd2lem  18666  psgndmsubg  19493  dsmmbas2  21724  dsmmelbas  21726  islindf4  21825  restbas  23131  ptval  23543  kqcldsat  23706  kqnrmlem1  23716  kqnrmlem2  23717  hmphtop  23751  ustn0  24194  uniiccdif  25568  cpncn  25927  cpnres  25928  ulmf2  26382  tglngne  28513  uhgrn0  29031  upgrfn  29051  upgrex  29056  umgrfn  29063  fcoinver  32564  nfpconfp  32589  opprabs  33451  mdetpmtr1  33763  coinflipspace  34424  bnj945  34728  bnj545  34850  bnj548  34852  bnj570  34860  bnj900  34884  bnj929  34891  bnj983  34906  bnj1018g  34918  bnj1018  34919  bnj1110  34937  bnj1145  34948  bnj1245  34969  bnj1253  34972  bnj1286  34974  bnj1280  34975  bnj1296  34976  bnj1311  34979  bnj1450  35005  bnj1498  35016  bnj1514  35018  bnj1501  35022  dfrdg2  35737  heibor1lem  37757  aks6d1c2lem4  42069  eqresfnbd  42213  aomclem6  43016  tfsconcatun  43295  tfsconcatb0  43302  tfsconcat0i  43303  tfsconcat0b  43304  tfsconcatrev  43306  tfsnfin  43310  ntrclsfv1  44013  ntrneifv1  44037  fnresdmss  45118  dmmptif  45218  fnresfnco  46999  fnfocofob  47037  fnbrafvb  47112  uniimaprimaeqfv  47315  elsetpreimafvssdm  47319  imasetpreimafvbijlemfo  47338  fnxpdmdm  48022  plusfreseq  48026