Theorem fndm 6642

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5663  Fun wfun 6534   Fn wfn 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6543

This theorem is used by:  fndmi  6643  fndmd  6644  funfni  6645  fndmu  6646  fnbr  6647  fnunres1  6651  fncofn  6656  fnco  6657  fnresdm  6658  fnresdisj  6659  fnssresb  6661  fn0  6670  fnimadisj  6671  fnimaeq0  6672  f1odmOLD  6829  fvelimab  6957  fvun1  6976  eqfnfv2  7030  fndmdif  7041  fneqeql2  7046  elpreima  7057  fsn2  7136  fnsnbg  7168  fnprb  7213  fntpb  7214  fconst3  7218  fconst4  7219  fnfvima  7238  ralima  7242  fnunirn  7256  dff13  7257  nvof1o  7287  oprssov  7589  fnexALT  7954  curry1  8105  curry1val  8106  curry2  8108  curry2val  8110  fparlem3  8115  fparlem4  8116  offsplitfpar  8120  suppvalfng  8169  suppvalfn  8170  suppfnss  8191  fnsuppres  8193  tposfo2  8251  frrlem3  8291  frrlem4  8292  smodm2  8348  smoel2  8356  tfrlem8  8377  tfrlem9  8378  tfrlem9a  8379  tfrlem13  8383  tz7.44-3  8401  rdglim  8419  frsucmptn  8432  oaabs2  8641  omabs  8643  ixpprc  8923  undifixp  8938  bren  8959  fndmeng  9039  tfsnfin2  9327  inf0  9597  r1lim  9751  jech9.3  9793  ssrankr1  9814  rankuni  9842  dfac3  10121  cfsmolem  10269  fin23lem31  10342  itunitc1  10419  ituniiun  10421  fnct  10536  cfpwsdom  10584  grur1  10820  genpdm  11002  fsuppmapnn0fiublem  14044  fsuppmapnn0fiub  14045  hashfn  14429  cshimadifsn  14890  cshimadifsn0  14891  shftfn  15134  rlimi2  15589  phimullem  16860  restsspw  17506  prdsdsval  17553  fnpr2ob  17634  sscpwex  17894  sscfn1  17896  sscfn2  17897  isssc  17899  funcres  17975  xpcbas  18256  xpchomfval  18257  gsumpropd2lem  18769  psgndmsubg  19616  dsmmbas2  21937  dsmmelbas  21939  islindf4  22038  restbas  23365  ptval  23778  kqcldsat  23941  kqnrmlem1  23951  kqnrmlem2  23952  hmphtop  23986  ustn0  24429  uniiccdif  25788  cpncn  26146  cpnres  26147  ulmf2  26598  tglngne  28870  uhgrn0  29472  upgrfn  29492  upgrex  29497  umgrfn  29504  fcoinver  33020  fresunsn  33041  nfpconfp  33048  opprabs  33828  mdetpmtr1  34277  coinflipspace  34936  bnj945  35227  bnj545  35348  bnj548  35350  bnj570  35358  bnj900  35382  bnj929  35389  bnj983  35404  bnj1018g  35416  bnj1018  35417  bnj1110  35435  bnj1145  35446  bnj1245  35467  bnj1253  35470  bnj1286  35472  bnj1280  35473  bnj1296  35474  bnj1311  35477  bnj1450  35503  bnj1498  35514  bnj1514  35516  bnj1501  35520  dfrdg2  36322  heibor1lem  38518  aks6d1c2lem4  42952  eqresfnbd  43061  aomclem6  43844  tfsconcatun  44122  tfsconcatb0  44129  tfsconcat0i  44130  tfsconcat0b  44131  tfsconcatrev  44133  tfsnfin  44137  ntrclsfv1  44839  ntrneifv1  44863  fnresdmss  45944  dmmptif  46039  fnresfnco  47836  fnfocofob  47874  fnbrafvb  47949  uniimaprimaeqfv  48189  elsetpreimafvssdm  48193  imasetpreimafvbijlemfo  48212  fnxpdmdm  48982  plusfreseq  48986  dmdm  49888