Theorem fndm 6621

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638  Fun wfun 6505   Fn wfn 6506

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 6514

This theorem is referenced by:  fndmi  6622  fndmd  6623  funfni  6624  fndmu  6625  fnbr  6626  fnunres1  6630  fncofn  6635  fnco  6636  fnresdm  6637  fnresdisj  6638  fnssresb  6640  fn0  6649  fnimadisj  6650  fnimaeq0  6651  f1odm  6804  fvelimab  6933  fvun1  6952  eqfnfv2  7004  fndmdif  7014  fneqeql2  7019  elpreima  7030  fsn2  7108  fnsnbg  7138  fnprb  7182  fntpb  7183  fconst3  7187  fconst4  7188  fnfvima  7207  ralima  7211  fnunirn  7228  dff13  7229  nvof1o  7255  oprssov  7558  fnexALT  7929  curry1  8083  curry1val  8084  curry2  8086  curry2val  8088  fparlem3  8093  fparlem4  8094  offsplitfpar  8098  suppvalfng  8146  suppvalfn  8147  suppfnss  8168  fnsuppres  8170  tposfo2  8228  frrlem3  8267  frrlem4  8268  smodm2  8324  smoel2  8332  tfrlem8  8352  tfrlem9  8353  tfrlem9a  8354  tfrlem13  8358  tz7.44-3  8376  rdglim  8394  frsucmptn  8407  oaabs2  8613  omabs  8615  ixpprc  8892  undifixp  8907  bren  8928  fndmeng  9006  inf0  9574  r1lim  9725  jech9.3  9767  ssrankr1  9788  rankuni  9816  dfac3  10074  cfsmolem  10223  fin23lem31  10296  itunitc1  10373  ituniiun  10375  fnct  10490  cfpwsdom  10537  grur1  10773  genpdm  10955  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  hashfn  14340  cshimadifsn  14795  cshimadifsn0  14796  shftfn  15039  rlimi2  15480  phimullem  16749  restsspw  17394  prdsdsval  17441  fnpr2ob  17521  sscpwex  17777  sscfn1  17779  sscfn2  17780  isssc  17782  funcres  17858  xpcbas  18139  xpchomfval  18140  gsumpropd2lem  18606  psgndmsubg  19432  dsmmbas2  21646  dsmmelbas  21648  islindf4  21747  restbas  23045  ptval  23457  kqcldsat  23620  kqnrmlem1  23630  kqnrmlem2  23631  hmphtop  23665  ustn0  24108  uniiccdif  25479  cpncn  25838  cpnres  25839  ulmf2  26293  tglngne  28477  uhgrn0  28994  upgrfn  29014  upgrex  29019  umgrfn  29026  fcoinver  32533  nfpconfp  32556  opprabs  33453  mdetpmtr1  33813  coinflipspace  34472  bnj945  34763  bnj545  34885  bnj548  34887  bnj570  34895  bnj900  34919  bnj929  34926  bnj983  34941  bnj1018g  34953  bnj1018  34954  bnj1110  34972  bnj1145  34983  bnj1245  35004  bnj1253  35007  bnj1286  35009  bnj1280  35010  bnj1296  35011  bnj1311  35014  bnj1450  35040  bnj1498  35051  bnj1514  35053  bnj1501  35057  dfrdg2  35783  heibor1lem  37803  aks6d1c2lem4  42115  eqresfnbd  42220  aomclem6  43048  tfsconcatun  43326  tfsconcatb0  43333  tfsconcat0i  43334  tfsconcat0b  43335  tfsconcatrev  43337  tfsnfin  43341  ntrclsfv1  44044  ntrneifv1  44068  fnresdmss  45162  dmmptif  45260  fnresfnco  47042  fnfocofob  47080  fnbrafvb  47155  uniimaprimaeqfv  47383  elsetpreimafvssdm  47387  imasetpreimafvbijlemfo  47406  fnxpdmdm  48148  plusfreseq  48152  dmdm  49042