Theorem fndm 6596

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5625  Fun wfun 6487   Fn wfn 6488

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 6496

This theorem is referenced by:  fndmi  6597  fndmd  6598  funfni  6599  fndmu  6600  fnbr  6601  fnunres1  6605  fncofn  6610  fnco  6611  fnresdm  6612  fnresdisj  6613  fnssresb  6615  fn0  6624  fnimadisj  6625  fnimaeq0  6626  f1odm  6779  fvelimab  6907  fvun1  6926  eqfnfv2  6979  fndmdif  6989  fneqeql2  6994  elpreima  7005  fsn2  7084  fnsnbg  7113  fnprb  7157  fntpb  7158  fconst3  7162  fconst4  7163  fnfvima  7182  ralima  7186  fnunirn  7202  dff13  7203  nvof1o  7229  oprssov  7530  fnexALT  7898  curry1  8048  curry1val  8049  curry2  8051  curry2val  8053  fparlem3  8058  fparlem4  8059  offsplitfpar  8063  suppvalfng  8111  suppvalfn  8112  suppfnss  8133  fnsuppres  8135  tposfo2  8193  frrlem3  8232  frrlem4  8233  smodm2  8289  smoel2  8297  tfrlem8  8317  tfrlem9  8318  tfrlem9a  8319  tfrlem13  8323  tz7.44-3  8341  rdglim  8359  frsucmptn  8372  oaabs2  8579  omabs  8581  ixpprc  8861  undifixp  8876  bren  8897  fndmeng  8976  tfsnfin2  9267  inf0  9536  r1lim  9690  jech9.3  9732  ssrankr1  9753  rankuni  9781  dfac3  10037  cfsmolem  10186  fin23lem31  10259  itunitc1  10336  ituniiun  10338  fnct  10453  cfpwsdom  10501  grur1  10737  genpdm  10919  fsuppmapnn0fiublem  13946  fsuppmapnn0fiub  13947  hashfn  14331  cshimadifsn  14785  cshimadifsn0  14786  shftfn  15029  rlimi2  15470  phimullem  16743  restsspw  17388  prdsdsval  17435  fnpr2ob  17516  sscpwex  17776  sscfn1  17778  sscfn2  17779  isssc  17781  funcres  17857  xpcbas  18138  xpchomfval  18139  gsumpropd2lem  18641  psgndmsubg  19471  dsmmbas2  21730  dsmmelbas  21732  islindf4  21831  restbas  23136  ptval  23548  kqcldsat  23711  kqnrmlem1  23721  kqnrmlem2  23722  hmphtop  23756  ustn0  24199  uniiccdif  25558  cpncn  25916  cpnres  25917  ulmf2  26365  tglngne  28635  uhgrn0  29153  upgrfn  29173  upgrex  29178  umgrfn  29185  fcoinver  32692  fresunsn  32716  nfpconfp  32723  opprabs  33560  mdetpmtr1  33986  coinflipspace  34644  bnj945  34935  bnj545  35056  bnj548  35058  bnj570  35066  bnj900  35090  bnj929  35097  bnj983  35112  bnj1018g  35124  bnj1018  35125  bnj1110  35143  bnj1145  35154  bnj1245  35175  bnj1253  35178  bnj1286  35180  bnj1280  35181  bnj1296  35182  bnj1311  35185  bnj1450  35211  bnj1498  35222  bnj1514  35224  bnj1501  35228  dfrdg2  35994  heibor1lem  38147  aks6d1c2lem4  42583  eqresfnbd  42690  aomclem6  43508  tfsconcatun  43786  tfsconcatb0  43793  tfsconcat0i  43794  tfsconcat0b  43795  tfsconcatrev  43797  tfsnfin  43801  ntrclsfv1  44503  ntrneifv1  44527  fnresdmss  45619  dmmptif  45716  fnresfnco  47504  fnfocofob  47542  fnbrafvb  47617  uniimaprimaeqfv  47857  elsetpreimafvssdm  47861  imasetpreimafvbijlemfo  47880  fnxpdmdm  48651  plusfreseq  48655  dmdm  49543