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

Theorem fndm 6610
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 6504 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 498 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  dom cdm 5638  Fun wfun 6495   Fn wfn 6496
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 398  df-fn 6504
This theorem is referenced by:  fndmi  6611  fndmd  6612  funfni  6613  fndmu  6614  fnbr  6615  fncofn  6622  fnco  6623  fncoOLD  6624  fnresdm  6625  fnresdisj  6626  fnssresb  6628  fn0  6637  fnimadisj  6638  fnimaeq0  6639  fdmOLD  6683  f1dmOLD  6748  f1odm  6793  fvelimab  6919  fvun1  6937  eqfnfv2  6988  fndmdif  6997  fneqeql2  7002  elpreima  7013  fsn2  7087  fnprb  7163  fntpb  7164  fconst3  7168  fconst4  7169  fnfvima  7188  fnunirn  7206  dff13  7207  nvof1o  7231  f1eqcocnvOLD  7253  oprssov  7528  fnexALT  7888  dmmpogaOLD  8011  curry1  8041  curry1val  8042  curry2  8044  curry2val  8046  fparlem3  8051  fparlem4  8052  offsplitfpar  8056  suppvalfng  8104  suppvalfn  8105  suppfnss  8125  fnsuppres  8127  tposfo2  8185  frrlem3  8224  frrlem4  8225  wfrlem3OLD  8261  wfrlem4OLD  8263  wfrdmclOLD  8268  wfrlem12OLD  8271  smodm2  8306  smoel2  8314  tfrlem8  8335  tfrlem9  8336  tfrlem9a  8337  tfrlem13  8341  tz7.44-3  8359  rdglim  8377  frsucmptn  8390  oaabs2  8600  omabs  8602  ixpprc  8864  undifixp  8879  bren  8900  brenOLD  8901  fndmeng  8986  inf0  9564  r1lim  9715  jech9.3  9757  ssrankr1  9778  rankuni  9806  dfac3  10064  cfsmolem  10213  fin23lem31  10286  itunitc1  10363  ituniiun  10365  fnct  10480  cfpwsdom  10527  grur1  10763  genpdm  10945  fsuppmapnn0fiublem  13902  fsuppmapnn0fiub  13903  hashfn  14282  cshimadifsn  14725  cshimadifsn0  14726  shftfn  14965  rlimi2  15403  phimullem  16658  restsspw  17320  prdsdsval  17367  fnpr2ob  17447  sscpwex  17705  sscfn1  17707  sscfn2  17708  isssc  17710  funcres  17789  xpcbas  18073  xpchomfval  18074  gsumpropd2lem  18541  psgndmsubg  19291  dsmmbas2  21159  dsmmelbas  21161  islindf4  21260  restbas  22525  ptval  22937  kqcldsat  23100  kqnrmlem1  23110  kqnrmlem2  23111  hmphtop  23145  ustn0  23588  uniiccdif  24958  cpncn  25316  cpnres  25317  ulmf2  25759  tglngne  27534  uhgrn0  28060  upgrfn  28080  upgrex  28085  umgrfn  28092  fnunres1  31566  fcoinver  31567  nfpconfp  31588  mdetpmtr1  32444  coinflipspace  33120  bnj945  33425  bnj545  33547  bnj548  33549  bnj570  33557  bnj900  33581  bnj929  33588  bnj983  33603  bnj1018g  33615  bnj1018  33616  bnj1110  33634  bnj1145  33645  bnj1245  33666  bnj1253  33669  bnj1286  33671  bnj1280  33672  bnj1296  33673  bnj1311  33676  bnj1450  33702  bnj1498  33713  bnj1514  33715  bnj1501  33719  dfrdg2  34409  heibor1lem  36297  fnsnbt  40686  aomclem6  41415  ntrclsfv1  42401  ntrneifv1  42425  fnresdmss  43459  dmmptif  43569  fnresfnco  45349  fnfocofob  45385  fnbrafvb  45460  uniimaprimaeqfv  45648  elsetpreimafvssdm  45652  imasetpreimafvbijlemfo  45671  fnxpdmdm  46136  plusfreseq  46140
  Copyright terms: Public domain W3C validator