Theorem fndm 6603

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5632  Fun wfun 6494   Fn wfn 6495

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 6503

This theorem is referenced by:  fndmi  6604  fndmd  6605  funfni  6606  fndmu  6607  fnbr  6608  fnunres1  6612  fncofn  6617  fnco  6618  fnresdm  6619  fnresdisj  6620  fnssresb  6622  fn0  6631  fnimadisj  6632  fnimaeq0  6633  f1odm  6786  fvelimab  6914  fvun1  6933  eqfnfv2  6986  fndmdif  6996  fneqeql2  7001  elpreima  7012  fsn2  7091  fnsnbg  7120  fnprb  7164  fntpb  7165  fconst3  7169  fconst4  7170  fnfvima  7189  ralima  7193  fnunirn  7209  dff13  7210  nvof1o  7236  oprssov  7537  fnexALT  7905  curry1  8056  curry1val  8057  curry2  8059  curry2val  8061  fparlem3  8066  fparlem4  8067  offsplitfpar  8071  suppvalfng  8119  suppvalfn  8120  suppfnss  8141  fnsuppres  8143  tposfo2  8201  frrlem3  8240  frrlem4  8241  smodm2  8297  smoel2  8305  tfrlem8  8325  tfrlem9  8326  tfrlem9a  8327  tfrlem13  8331  tz7.44-3  8349  rdglim  8367  frsucmptn  8380  oaabs2  8587  omabs  8589  ixpprc  8869  undifixp  8884  bren  8905  fndmeng  8984  tfsnfin2  9275  inf0  9542  r1lim  9696  jech9.3  9738  ssrankr1  9759  rankuni  9787  dfac3  10043  cfsmolem  10192  fin23lem31  10265  itunitc1  10342  ituniiun  10344  fnct  10459  cfpwsdom  10507  grur1  10743  genpdm  10925  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  hashfn  14310  cshimadifsn  14764  cshimadifsn0  14765  shftfn  15008  rlimi2  15449  phimullem  16718  restsspw  17363  prdsdsval  17410  fnpr2ob  17491  sscpwex  17751  sscfn1  17753  sscfn2  17754  isssc  17756  funcres  17832  xpcbas  18113  xpchomfval  18114  gsumpropd2lem  18616  psgndmsubg  19443  dsmmbas2  21704  dsmmelbas  21706  islindf4  21805  restbas  23114  ptval  23526  kqcldsat  23689  kqnrmlem1  23699  kqnrmlem2  23700  hmphtop  23734  ustn0  24177  uniiccdif  25547  cpncn  25906  cpnres  25907  ulmf2  26361  tglngne  28634  uhgrn0  29152  upgrfn  29172  upgrex  29177  umgrfn  29184  fcoinver  32691  fresunsn  32715  nfpconfp  32722  opprabs  33575  mdetpmtr1  34001  coinflipspace  34659  bnj945  34950  bnj545  35071  bnj548  35073  bnj570  35081  bnj900  35105  bnj929  35112  bnj983  35127  bnj1018g  35139  bnj1018  35140  bnj1110  35158  bnj1145  35169  bnj1245  35190  bnj1253  35193  bnj1286  35195  bnj1280  35196  bnj1296  35197  bnj1311  35200  bnj1450  35226  bnj1498  35237  bnj1514  35239  bnj1501  35243  dfrdg2  36009  heibor1lem  38060  aks6d1c2lem4  42497  eqresfnbd  42604  aomclem6  43416  tfsconcatun  43694  tfsconcatb0  43701  tfsconcat0i  43702  tfsconcat0b  43703  tfsconcatrev  43705  tfsnfin  43709  ntrclsfv1  44411  ntrneifv1  44435  fnresdmss  45527  dmmptif  45624  fnresfnco  47401  fnfocofob  47439  fnbrafvb  47514  uniimaprimaeqfv  47742  elsetpreimafvssdm  47746  imasetpreimafvbijlemfo  47765  fnxpdmdm  48520  plusfreseq  48524  dmdm  49412