Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fndm Structured version   Visualization version   GIF version

Theorem fndm 6426
 Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 6328 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 500 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  dom cdm 5520  Fun wfun 6319   Fn wfn 6320 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 210  df-an 400  df-fn 6328 This theorem is referenced by:  fndmi  6427  fndmd  6428  funfni  6429  fndmu  6430  fnbr  6431  fnco  6438  fnresdm  6439  fnresdisj  6440  fnssresb  6442  fn0  6452  fnimadisj  6453  fnimaeq0  6454  fdmOLD  6497  f1dmOLD  6555  f1odm  6595  fvelimab  6713  fvun1  6730  eqfnfv2  6781  fndmdif  6790  fneqeql2  6795  elpreima  6806  fsn2  6876  fnprb  6949  fntpb  6950  fconst3  6954  fconst4  6955  fnfvima  6974  fnunirn  6991  dff13  6992  nvof1o  7016  f1eqcocnvOLD  7037  oprssov  7299  fnexALT  7637  dmmpogaOLD  7757  curry1  7785  curry1val  7786  curry2  7788  curry2val  7790  fparlem3  7795  fparlem4  7796  offsplitfpar  7801  suppvalfn  7823  suppfnss  7841  fnsuppres  7843  tposfo2  7901  wfrlem3  7942  wfrlem4  7944  wfrdmcl  7949  wfrlem12  7952  smodm2  7978  smoel2  7986  tfrlem8  8006  tfrlem9  8007  tfrlem9a  8008  tfrlem13  8012  tz7.44-3  8030  rdglim  8048  frsucmptn  8060  oaabs2  8258  omabs  8260  ixpprc  8469  undifixp  8484  bren  8504  fndmeng  8573  inf0  9071  r1lim  9188  jech9.3  9230  ssrankr1  9251  rankuni  9279  dfac3  9535  cfsmolem  9684  fin23lem31  9757  itunitc1  9834  ituniiun  9836  fnct  9951  cfpwsdom  9998  grur1  10234  genpdm  10416  fsuppmapnn0fiublem  13356  fsuppmapnn0fiub  13357  hashfn  13735  cshimadifsn  14185  cshimadifsn0  14186  shftfn  14427  rlimi2  14866  phimullem  16109  restsspw  16700  prdsdsval  16746  fnpr2ob  16826  sscpwex  17080  sscfn1  17082  sscfn2  17083  isssc  17085  funcres  17161  xpcbas  17423  xpchomfval  17424  gsumpropd2lem  17884  psgndmsubg  18626  dsmmbas2  20431  dsmmelbas  20433  islindf4  20532  restbas  21773  ptval  22185  kqcldsat  22348  kqnrmlem1  22358  kqnrmlem2  22359  hmphtop  22393  ustn0  22836  uniiccdif  24192  cpncn  24549  cpnres  24550  ulmf2  24989  tglngne  26354  uhgrn0  26870  upgrfn  26890  upgrex  26895  umgrfn  26902  fnunres1  30379  fcoinver  30380  nfpconfp  30401  mdetpmtr1  31191  coinflipspace  31863  bnj945  32170  bnj545  32292  bnj548  32294  bnj570  32302  bnj900  32326  bnj929  32333  bnj983  32348  bnj1018g  32360  bnj1018  32361  bnj1110  32379  bnj1145  32390  bnj1245  32411  bnj1253  32414  bnj1286  32416  bnj1280  32417  bnj1296  32418  bnj1311  32421  bnj1450  32447  bnj1498  32458  bnj1514  32460  bnj1501  32464  dfrdg2  33168  frrlem3  33253  frrlem4  33254  heibor1lem  35266  fnsnbt  39434  aomclem6  40046  ntrclsfv1  40801  ntrneifv1  40825  fnresdmss  41835  fnresfnco  43676  fnbrafvb  43753  uniimaprimaeqfv  43942  elsetpreimafvssdm  43946  imasetpreimafvbijlemfo  43965  fnxpdmdm  44431  plusfreseq  44435
 Copyright terms: Public domain W3C validator