Theorem fndm 6645

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5666  Fun wfun 6537   Fn wfn 6538

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 6546

This theorem is used by:  fndmi  6646  fndmd  6647  funfni  6648  fndmu  6649  fnbr  6650  fnunres1  6654  fncofn  6659  fnco  6660  fnresdm  6661  fnresdisj  6662  fnssresb  6664  fn0  6673  fnimadisj  6674  fnimaeq0  6675  f1odmOLD  6832  fvelimab  6960  fvun1  6979  eqfnfv2  7033  fndmdif  7044  fneqeql2  7049  elpreima  7060  fsn2  7139  fnsnbg  7169  fnprb  7213  fntpb  7214  fconst3  7218  fconst4  7219  fnfvima  7238  ralima  7242  fnunirn  7258  dff13  7259  nvof1o  7289  oprssov  7592  fnexALT  7957  curry1  8108  curry1val  8109  curry2  8111  curry2val  8113  fparlem3  8118  fparlem4  8119  offsplitfpar  8123  suppvalfng  8172  suppvalfn  8173  suppfnss  8194  fnsuppres  8196  tposfo2  8254  frrlem3  8294  frrlem4  8295  smodm2  8351  smoel2  8359  tfrlem8  8380  tfrlem9  8381  tfrlem9a  8382  tfrlem13  8386  tz7.44-3  8404  rdglim  8422  frsucmptn  8435  oaabs2  8644  omabs  8646  ixpprc  8926  undifixp  8941  bren  8962  fndmeng  9042  tfsnfin2  9330  inf0  9600  r1lim  9754  jech9.3  9796  ssrankr1  9817  rankuni  9845  dfac3  10124  cfsmolem  10272  fin23lem31  10345  itunitc1  10422  ituniiun  10424  fnct  10539  cfpwsdom  10587  grur1  10823  genpdm  11005  fsuppmapnn0fiublem  14046  fsuppmapnn0fiub  14047  hashfn  14431  cshimadifsn  14892  cshimadifsn0  14893  shftfn  15136  rlimi2  15591  phimullem  16863  restsspw  17509  prdsdsval  17556  fnpr2ob  17637  sscpwex  17897  sscfn1  17899  sscfn2  17900  isssc  17902  funcres  17978  xpcbas  18259  xpchomfval  18260  gsumpropd2lem  18762  psgndmsubg  19597  dsmmbas2  21917  dsmmelbas  21919  islindf4  22018  restbas  23345  ptval  23757  kqcldsat  23920  kqnrmlem1  23930  kqnrmlem2  23931  hmphtop  23965  ustn0  24408  uniiccdif  25767  cpncn  26125  cpnres  26126  ulmf2  26577  tglngne  28849  uhgrn0  29447  upgrfn  29467  upgrex  29472  umgrfn  29479  fcoinver  32979  fresunsn  33000  nfpconfp  33007  opprabs  33788  mdetpmtr1  34237  coinflipspace  34895  bnj945  35186  bnj545  35307  bnj548  35309  bnj570  35317  bnj900  35341  bnj929  35348  bnj983  35363  bnj1018g  35375  bnj1018  35376  bnj1110  35394  bnj1145  35405  bnj1245  35426  bnj1253  35429  bnj1286  35431  bnj1280  35432  bnj1296  35433  bnj1311  35436  bnj1450  35462  bnj1498  35473  bnj1514  35475  bnj1501  35479  dfrdg2  36298  heibor1lem  38493  aks6d1c2lem4  42927  eqresfnbd  43036  aomclem6  43819  tfsconcatun  44097  tfsconcatb0  44104  tfsconcat0i  44105  tfsconcat0b  44106  tfsconcatrev  44108  tfsnfin  44112  ntrclsfv1  44814  ntrneifv1  44838  fnresdmss  45919  dmmptif  46014  fnresfnco  47811  fnfocofob  47849  fnbrafvb  47924  uniimaprimaeqfv  48164  elsetpreimafvssdm  48168  imasetpreimafvbijlemfo  48187  fnxpdmdm  48958  plusfreseq  48962  dmdm  49864