Theorem fndm 6640

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5651  Fun wfun 6531   Fn wfn 6532

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 6540

This theorem is used by:  fndmi  6641  fndmd  6642  funfni  6643  fndmu  6644  fnbr  6645  fnunres1  6649  fncofn  6654  fnco  6655  fnresdm  6656  fnresdisj  6657  fnssresb  6659  fn0  6668  fnimadisj  6669  fnimaeq0  6670  f1odmOLD  6827  fvelimab  6955  fvun1  6974  eqfnfv2  7028  fndmdif  7039  fneqeql2  7044  elpreima  7055  fsn2  7135  fnsnbg  7167  fnprb  7212  fntpb  7213  fconst3  7217  fconst4  7218  fnfvima  7237  ralima  7241  fnunirn  7255  dff13  7256  nvof1o  7286  oprssov  7588  fnexALT  7961  curry1  8113  curry1val  8114  curry2  8116  curry2val  8118  fparlem3  8123  fparlem4  8124  offsplitfpar  8128  suppvalfng  8177  suppvalfn  8178  suppfnss  8199  fnsuppres  8201  tposfo2  8259  frrlem3  8299  frrlem4  8300  smodm2  8356  smoel2  8364  tfrlem8  8385  tfrlem9  8386  tfrlem9a  8387  tfrlem13  8391  tz7.44-3  8409  rdglim  8427  frsucmptn  8440  oaabs2  8651  omabs  8653  ixpprc  8940  undifixp  8955  bren  8976  fndmeng  9056  tfsnfin2  9345  inf0  9615  jech9.3OLD  9816  ssrankr1  9840  rankuni  9872  dfac3  10193  cfsmolem  10341  fin23lem31  10414  itunitc1  10491  ituniiun  10493  fnct  10613  fnctOLD  10614  cfpwsdom  10662  grur1  10898  genpdm  11080  fsuppmapnn0fiublem  14126  fsuppmapnn0fiub  14127  hashfn  14512  cshimadifsn  14973  cshimadifsn0  14974  shftfn  15219  rlimi2  15674  phimullem  16949  restsspw  17595  prdsdsval  17642  fnpr2ob  17723  sscpwex  17983  sscfn1  17985  sscfn2  17986  isssc  17988  funcres  18064  xpcbas  18345  xpchomfval  18346  gsumpropd2lem  18861  psgndmsubg  19709  dsmmbas2  22036  dsmmelbas  22038  islindf4  22137  restbas  23469  ptval  23882  kqcldsat  24045  kqnrmlem1  24055  kqnrmlem2  24056  hmphtop  24090  ustn0  24533  uniiccdif  25892  cpncn  26249  cpnres  26250  ulmf2  26704  tglngne  29006  uhgrn0  29638  upgrfn  29658  upgrex  29663  umgrfn  29670  fcoinver  33191  fresunsn  33212  nfpconfp  33219  opprabs  33999  mdetpmtr1  34448  coinflipspace  35106  bnj945  35397  bnj545  35518  bnj548  35520  bnj570  35528  bnj900  35552  bnj929  35559  bnj983  35574  bnj1018g  35586  bnj1018  35587  bnj1110  35605  bnj1145  35616  bnj1245  35637  bnj1253  35640  bnj1286  35642  bnj1280  35643  bnj1296  35644  bnj1311  35647  bnj1450  35673  bnj1498  35684  bnj1514  35686  bnj1501  35690  dfrdg2  36537  heibor1lem  38723  aks6d1c2lem4  43157  eqresfnbd  43266  aomclem6  44045  tfsconcatun  44323  tfsconcatb0  44330  tfsconcat0i  44331  tfsconcat0b  44332  tfsconcatrev  44334  tfsnfin  44338  ntrclsfv1  45040  ntrneifv1  45064  fnresdmss  46152  dmmptif  46247  fnresfnco  48080  fnfocofob  48118  fnbrafvb  48193  uniimaprimaeqfv  48433  elsetpreimafvssdm  48437  imasetpreimafvbijlemfo  48456  fnxpdmdm  49226  plusfreseq  49230  dmdm  50130