Theorem fndm 6545

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5590  Fun wfun 6431   Fn wfn 6432

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 206  df-an 397  df-fn 6440

This theorem is referenced by:  fndmi  6546  fndmd  6547  funfni  6548  fndmu  6549  fnbr  6550  fncofn  6557  fnco  6558  fncoOLD  6559  fnresdm  6560  fnresdisj  6561  fnssresb  6563  fn0  6573  fnimadisj  6574  fnimaeq0  6575  fdmOLD  6619  f1dmOLD  6684  f1odm  6729  fvelimab  6850  fvun1  6868  eqfnfv2  6919  fndmdif  6928  fneqeql2  6933  elpreima  6944  fsn2  7017  fnprb  7093  fntpb  7094  fconst3  7098  fconst4  7099  fnfvima  7118  fnunirn  7136  dff13  7137  nvof1o  7161  f1eqcocnvOLD  7183  oprssov  7450  fnexALT  7802  dmmpogaOLD  7923  curry1  7953  curry1val  7954  curry2  7956  curry2val  7958  fparlem3  7963  fparlem4  7964  offsplitfpar  7969  suppvalfng  7993  suppvalfn  7994  suppfnss  8014  fnsuppres  8016  tposfo2  8074  frrlem3  8113  frrlem4  8114  wfrlem3OLD  8150  wfrlem4OLD  8152  wfrdmclOLD  8157  wfrlem12OLD  8160  smodm2  8195  smoel2  8203  tfrlem8  8224  tfrlem9  8225  tfrlem9a  8226  tfrlem13  8230  tz7.44-3  8248  rdglim  8266  frsucmptn  8279  oaabs2  8488  omabs  8490  ixpprc  8716  undifixp  8731  bren  8752  brenOLD  8753  fndmeng  8834  inf0  9388  r1lim  9539  jech9.3  9581  ssrankr1  9602  rankuni  9630  dfac3  9886  cfsmolem  10035  fin23lem31  10108  itunitc1  10185  ituniiun  10187  fnct  10302  cfpwsdom  10349  grur1  10585  genpdm  10767  fsuppmapnn0fiublem  13719  fsuppmapnn0fiub  13720  hashfn  14099  cshimadifsn  14551  cshimadifsn0  14552  shftfn  14793  rlimi2  15232  phimullem  16489  restsspw  17151  prdsdsval  17198  fnpr2ob  17278  sscpwex  17536  sscfn1  17538  sscfn2  17539  isssc  17541  funcres  17620  xpcbas  17904  xpchomfval  17905  gsumpropd2lem  18372  psgndmsubg  19119  dsmmbas2  20953  dsmmelbas  20955  islindf4  21054  restbas  22318  ptval  22730  kqcldsat  22893  kqnrmlem1  22903  kqnrmlem2  22904  hmphtop  22938  ustn0  23381  uniiccdif  24751  cpncn  25109  cpnres  25110  ulmf2  25552  tglngne  26920  uhgrn0  27446  upgrfn  27466  upgrex  27471  umgrfn  27478  fnunres1  30954  fcoinver  30955  nfpconfp  30976  mdetpmtr1  31782  coinflipspace  32456  bnj945  32762  bnj545  32884  bnj548  32886  bnj570  32894  bnj900  32918  bnj929  32925  bnj983  32940  bnj1018g  32952  bnj1018  32953  bnj1110  32971  bnj1145  32982  bnj1245  33003  bnj1253  33006  bnj1286  33008  bnj1280  33009  bnj1296  33010  bnj1311  33013  bnj1450  33039  bnj1498  33050  bnj1514  33052  bnj1501  33056  dfrdg2  33780  heibor1lem  35976  fnsnbt  40215  aomclem6  40891  ntrclsfv1  41672  ntrneifv1  41696  fnresdmss  42711  fnresfnco  44546  fnfocofob  44582  fnbrafvb  44657  uniimaprimaeqfv  44845  elsetpreimafvssdm  44849  imasetpreimafvbijlemfo  44868  fnxpdmdm  45333  plusfreseq  45337