Theorem fndm 6635

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  Fun wfun 6527   Fn wfn 6528

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 6536

This theorem is used by:  fndmi  6636  fndmd  6637  funfni  6638  fndmu  6639  fnbr  6640  fnunres1  6644  fncofn  6649  fnco  6650  fnresdm  6651  fnresdisj  6652  fnssresb  6654  fn0  6663  fnimadisj  6664  fnimaeq0  6665  f1odmOLD  6822  fvelimab  6950  fvun1  6969  eqfnfv2  7023  fndmdif  7034  fneqeql2  7039  elpreima  7050  fsn2  7130  fnsnbg  7162  fnprb  7207  fntpb  7208  fconst3  7212  fconst4  7213  fnfvima  7232  ralima  7236  fnunirn  7250  dff13  7251  nvof1o  7281  oprssov  7583  fnexALT  7948  curry1  8101  curry1val  8102  curry2  8104  curry2val  8106  fparlem3  8111  fparlem4  8112  offsplitfpar  8116  suppvalfng  8165  suppvalfn  8166  suppfnss  8187  fnsuppres  8189  tposfo2  8247  frrlem3  8287  frrlem4  8288  smodm2  8344  smoel2  8352  tfrlem8  8373  tfrlem9  8374  tfrlem9a  8375  tfrlem13  8379  tz7.44-3  8397  rdglim  8415  frsucmptn  8428  oaabs2  8637  omabs  8639  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  10544  fnctOLD  10545  cfpwsdom  10593  grur1  10829  genpdm  11011  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  hashfn  14439  cshimadifsn  14900  cshimadifsn0  14901  shftfn  15146  rlimi2  15601  phimullem  16870  restsspw  17516  prdsdsval  17563  fnpr2ob  17644  sscpwex  17904  sscfn1  17906  sscfn2  17907  isssc  17909  funcres  17985  xpcbas  18266  xpchomfval  18267  gsumpropd2lem  18781  psgndmsubg  19629  dsmmbas2  21950  dsmmelbas  21952  islindf4  22051  restbas  23383  ptval  23796  kqcldsat  23959  kqnrmlem1  23969  kqnrmlem2  23970  hmphtop  24004  ustn0  24447  uniiccdif  25806  cpncn  26163  cpnres  26164  ulmf2  26620  tglngne  28892  uhgrn0  29524  upgrfn  29544  upgrex  29549  umgrfn  29556  fcoinver  33077  fresunsn  33098  nfpconfp  33105  opprabs  33884  mdetpmtr1  34333  coinflipspace  34992  bnj945  35283  bnj545  35404  bnj548  35406  bnj570  35414  bnj900  35438  bnj929  35445  bnj983  35460  bnj1018g  35472  bnj1018  35473  bnj1110  35491  bnj1145  35502  bnj1245  35523  bnj1253  35526  bnj1286  35528  bnj1280  35529  bnj1296  35530  bnj1311  35533  bnj1450  35559  bnj1498  35570  bnj1514  35572  bnj1501  35576  dfrdg2  36372  heibor1lem  38559  aks6d1c2lem4  42993  eqresfnbd  43102  aomclem6  43900  tfsconcatun  44178  tfsconcatb0  44185  tfsconcat0i  44186  tfsconcat0b  44187  tfsconcatrev  44189  tfsnfin  44193  ntrclsfv1  44895  ntrneifv1  44919  fnresdmss  46000  dmmptif  46095  fnresfnco  47929  fnfocofob  47967  fnbrafvb  48042  uniimaprimaeqfv  48282  elsetpreimafvssdm  48286  imasetpreimafvbijlemfo  48305  fnxpdmdm  49075  plusfreseq  49079  dmdm  49979