Theorem fndm 6588

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

Syntax hints:   → wi 4   = wceq 1547  dom cdm 5618  Fun wfun 6479   Fn wfn 6480

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 208  df-an 397  df-fn 6488

This theorem is referenced by:  fndmi  6589  fndmd  6590  funfni  6591  fndmu  6592  fnbr  6593  fnunres1  6597  fncofn  6602  fnco  6603  fnresdm  6604  fnresdisj  6605  fnssresb  6607  fn0  6616  fnimadisj  6617  fnimaeq0  6618  f1odm  6771  fvelimab  6899  fvun1  6918  eqfnfv2  6972  fndmdif  6983  fneqeql2  6988  elpreima  6999  fsn2  7078  fnsnbg  7108  fnprb  7152  fntpb  7153  fconst3  7157  fconst4  7158  fnfvima  7177  ralima  7181  fnunirn  7197  dff13  7198  nvof1o  7224  oprssov  7525  fnexALT  7893  curry1  8043  curry1val  8044  curry2  8046  curry2val  8048  fparlem3  8053  fparlem4  8054  offsplitfpar  8058  suppvalfng  8107  suppvalfn  8108  suppfnss  8129  fnsuppres  8131  tposfo2  8189  frrlem3  8228  frrlem4  8229  smodm2  8285  smoel2  8293  tfrlem8  8313  tfrlem9  8314  tfrlem9a  8315  tfrlem13  8319  tz7.44-3  8337  rdglim  8355  frsucmptn  8368  oaabs2  8575  omabs  8577  ixpprc  8857  undifixp  8872  bren  8893  fndmeng  8972  tfsnfin2  9263  inf0  9533  r1lim  9687  jech9.3  9729  ssrankr1  9750  rankuni  9778  dfac3  10034  cfsmolem  10183  fin23lem31  10256  itunitc1  10333  ituniiun  10335  fnct  10450  cfpwsdom  10498  grur1  10734  genpdm  10916  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  hashfn  14328  cshimadifsn  14782  cshimadifsn0  14783  shftfn  15026  rlimi2  15467  phimullem  16740  restsspw  17385  prdsdsval  17432  fnpr2ob  17513  sscpwex  17773  sscfn1  17775  sscfn2  17776  isssc  17778  funcres  17854  xpcbas  18135  xpchomfval  18136  gsumpropd2lem  18638  psgndmsubg  19468  dsmmbas2  21712  dsmmelbas  21714  islindf4  21813  restbas  23141  ptval  23553  kqcldsat  23716  kqnrmlem1  23726  kqnrmlem2  23727  hmphtop  23761  ustn0  24204  uniiccdif  25563  cpncn  25921  cpnres  25922  ulmf2  26367  tglngne  28636  uhgrn0  29154  upgrfn  29174  upgrex  29179  umgrfn  29186  fcoinver  32693  fresunsn  32717  nfpconfp  32724  opprabs  33565  mdetpmtr1  34007  coinflipspace  34665  bnj945  34956  bnj545  35077  bnj548  35079  bnj570  35087  bnj900  35111  bnj929  35118  bnj983  35133  bnj1018g  35145  bnj1018  35146  bnj1110  35164  bnj1145  35175  bnj1245  35196  bnj1253  35199  bnj1286  35201  bnj1280  35202  bnj1296  35203  bnj1311  35206  bnj1450  35232  bnj1498  35243  bnj1514  35245  bnj1501  35249  dfrdg2  36021  heibor1lem  38176  aks6d1c2lem4  42612  eqresfnbd  42719  aomclem6  43504  tfsconcatun  43782  tfsconcatb0  43789  tfsconcat0i  43790  tfsconcat0b  43791  tfsconcatrev  43793  tfsnfin  43797  ntrclsfv1  44499  ntrneifv1  44523  fnresdmss  45615  dmmptif  45710  fnresfnco  47504  fnfocofob  47542  fnbrafvb  47617  uniimaprimaeqfv  47857  elsetpreimafvssdm  47861  imasetpreimafvbijlemfo  47880  fnxpdmdm  48651  plusfreseq  48655  dmdm  49543