Theorem fndm 6593

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5622  Fun wfun 6484   Fn wfn 6485

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 6493

This theorem is referenced by:  fndmi  6594  fndmd  6595  funfni  6596  fndmu  6597  fnbr  6598  fnunres1  6602  fncofn  6607  fnco  6608  fnresdm  6609  fnresdisj  6610  fnssresb  6612  fn0  6621  fnimadisj  6622  fnimaeq0  6623  f1odm  6776  fvelimab  6904  fvun1  6923  eqfnfv2  6975  fndmdif  6985  fneqeql2  6990  elpreima  7001  fsn2  7079  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  8044  curry1val  8045  curry2  8047  curry2val  8049  fparlem3  8054  fparlem4  8055  offsplitfpar  8059  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  8855  undifixp  8870  bren  8891  fndmeng  8970  tfsnfin2  9261  inf0  9528  r1lim  9682  jech9.3  9724  ssrankr1  9745  rankuni  9773  dfac3  10029  cfsmolem  10178  fin23lem31  10251  itunitc1  10328  ituniiun  10330  fnct  10445  cfpwsdom  10493  grur1  10729  genpdm  10911  fsuppmapnn0fiublem  13911  fsuppmapnn0fiub  13912  hashfn  14296  cshimadifsn  14750  cshimadifsn0  14751  shftfn  14994  rlimi2  15435  phimullem  16704  restsspw  17349  prdsdsval  17396  fnpr2ob  17477  sscpwex  17737  sscfn1  17739  sscfn2  17740  isssc  17742  funcres  17818  xpcbas  18099  xpchomfval  18100  gsumpropd2lem  18602  psgndmsubg  19429  dsmmbas2  21690  dsmmelbas  21692  islindf4  21791  restbas  23100  ptval  23512  kqcldsat  23675  kqnrmlem1  23685  kqnrmlem2  23686  hmphtop  23720  ustn0  24163  uniiccdif  25533  cpncn  25892  cpnres  25893  ulmf2  26347  tglngne  28571  uhgrn0  29089  upgrfn  29109  upgrex  29114  umgrfn  29121  fcoinver  32628  fresunsn  32652  nfpconfp  32659  opprabs  33512  mdetpmtr1  33929  coinflipspace  34587  bnj945  34878  bnj545  35000  bnj548  35002  bnj570  35010  bnj900  35034  bnj929  35041  bnj983  35056  bnj1018g  35068  bnj1018  35069  bnj1110  35087  bnj1145  35098  bnj1245  35119  bnj1253  35122  bnj1286  35124  bnj1280  35125  bnj1296  35126  bnj1311  35129  bnj1450  35155  bnj1498  35166  bnj1514  35168  bnj1501  35172  dfrdg2  35936  heibor1lem  37949  aks6d1c2lem4  42320  eqresfnbd  42430  aomclem6  43243  tfsconcatun  43521  tfsconcatb0  43528  tfsconcat0i  43529  tfsconcat0b  43530  tfsconcatrev  43532  tfsnfin  43536  ntrclsfv1  44238  ntrneifv1  44262  fnresdmss  45354  dmmptif  45452  fnresfnco  47229  fnfocofob  47267  fnbrafvb  47342  uniimaprimaeqfv  47570  elsetpreimafvssdm  47574  imasetpreimafvbijlemfo  47593  fnxpdmdm  48348  plusfreseq  48352  dmdm  49240