Theorem fndm 6672

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5689  Fun wfun 6557   Fn wfn 6558

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 6566

This theorem is referenced by:  fndmi  6673  fndmd  6674  funfni  6675  fndmu  6676  fnbr  6677  fnunres1  6681  fncofn  6686  fnco  6687  fnresdm  6688  fnresdisj  6689  fnssresb  6691  fn0  6700  fnimadisj  6701  fnimaeq0  6702  f1odm  6853  fvelimab  6981  fvun1  7000  eqfnfv2  7052  fndmdif  7062  fneqeql2  7067  elpreima  7078  fsn2  7156  fnprb  7228  fntpb  7229  fconst3  7233  fconst4  7234  fnfvima  7253  ralima  7257  fnunirn  7274  dff13  7275  nvof1o  7300  oprssov  7602  fnexALT  7974  curry1  8128  curry1val  8129  curry2  8131  curry2val  8133  fparlem3  8138  fparlem4  8139  offsplitfpar  8143  suppvalfng  8191  suppvalfn  8192  suppfnss  8213  fnsuppres  8215  tposfo2  8273  frrlem3  8312  frrlem4  8313  wfrlem3OLD  8349  wfrlem4OLD  8351  wfrdmclOLD  8356  wfrlem12OLD  8359  smodm2  8394  smoel2  8402  tfrlem8  8423  tfrlem9  8424  tfrlem9a  8425  tfrlem13  8429  tz7.44-3  8447  rdglim  8465  frsucmptn  8478  oaabs2  8686  omabs  8688  ixpprc  8958  undifixp  8973  bren  8994  fndmeng  9074  inf0  9659  r1lim  9810  jech9.3  9852  ssrankr1  9873  rankuni  9901  dfac3  10159  cfsmolem  10308  fin23lem31  10381  itunitc1  10458  ituniiun  10460  fnct  10575  cfpwsdom  10622  grur1  10858  genpdm  11040  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  hashfn  14411  cshimadifsn  14865  cshimadifsn0  14866  shftfn  15109  rlimi2  15547  phimullem  16813  restsspw  17478  prdsdsval  17525  fnpr2ob  17605  sscpwex  17863  sscfn1  17865  sscfn2  17866  isssc  17868  funcres  17947  xpcbas  18234  xpchomfval  18235  gsumpropd2lem  18705  psgndmsubg  19535  dsmmbas2  21775  dsmmelbas  21777  islindf4  21876  restbas  23182  ptval  23594  kqcldsat  23757  kqnrmlem1  23767  kqnrmlem2  23768  hmphtop  23802  ustn0  24245  uniiccdif  25627  cpncn  25987  cpnres  25988  ulmf2  26442  tglngne  28573  uhgrn0  29099  upgrfn  29119  upgrex  29124  umgrfn  29131  fcoinver  32624  nfpconfp  32649  opprabs  33490  mdetpmtr1  33784  coinflipspace  34462  bnj945  34766  bnj545  34888  bnj548  34890  bnj570  34898  bnj900  34922  bnj929  34929  bnj983  34944  bnj1018g  34956  bnj1018  34957  bnj1110  34975  bnj1145  34986  bnj1245  35007  bnj1253  35010  bnj1286  35012  bnj1280  35013  bnj1296  35014  bnj1311  35017  bnj1450  35043  bnj1498  35054  bnj1514  35056  bnj1501  35060  dfrdg2  35777  heibor1lem  37796  aks6d1c2lem4  42109  fnsnbt  42250  eqresfnbd  42252  aomclem6  43048  tfsconcatun  43327  tfsconcatb0  43334  tfsconcat0i  43335  tfsconcat0b  43336  tfsconcatrev  43338  tfsnfin  43342  ntrclsfv1  44045  ntrneifv1  44069  fnresdmss  45111  dmmptif  45212  fnresfnco  46991  fnfocofob  47029  fnbrafvb  47104  uniimaprimaeqfv  47307  elsetpreimafvssdm  47311  imasetpreimafvbijlemfo  47330  fnxpdmdm  48004  plusfreseq  48008