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

Theorem fndm 6151
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 6052 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 483 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  dom cdm 5266  Fun wfun 6043   Fn wfn 6044
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 197  df-an 385  df-fn 6052
This theorem is referenced by:  funfni  6152  fndmu  6153  fnbr  6154  fnco  6160  fnresdm  6161  fnresdisj  6162  fnssresb  6164  fn0  6172  fnimadisj  6173  fnimaeq0  6174  dmmpti  6184  fdm  6212  f1dm  6266  f1odm  6302  f1o00  6332  fvelimab  6415  fvun1  6431  eqfnfv2  6475  fndmdif  6484  fneqeql2  6489  elpreima  6500  fsn2  6566  fnprb  6636  fntpb  6637  fconst3  6641  fconst4  6642  fnfvima  6659  fnunirn  6674  dff13  6675  nvof1o  6699  f1eqcocnv  6719  oprssov  6968  offval  7069  ofrfval  7070  fnexALT  7297  dmmpt2  7408  dmmpt2ga  7410  curry1  7437  curry1val  7438  curry2  7440  curry2val  7442  fparlem3  7447  fparlem4  7448  fnwelem  7460  suppvalfn  7470  suppfnss  7488  suppfnssOLD  7489  fnsuppres  7491  tposfo2  7544  wfrlem3  7585  wfrlem4  7587  wfrdmcl  7592  wfrlem12  7595  wfrlem17  7600  smodm2  7621  smoel2  7629  tfrlem5  7645  tfrlem8  7649  tfrlem9  7650  tfrlem9a  7651  tfrlem13  7655  tfr2  7663  tz7.44-2  7672  tz7.44-3  7673  rdgsuc  7689  rdglim  7691  frsucmptn  7703  tz7.48-2  7706  tz7.48-1  7707  tz7.48-3  7708  tz7.49  7709  brwitnlem  7756  om0x  7768  oaabs2  7894  omabs  7896  elpmi  8042  elmapex  8044  pmresg  8051  pmsspw  8058  ixpprc  8095  undifixp  8110  bren  8130  fndmeng  8199  wemapso  8621  ixpiunwdom  8661  inf0  8691  r1suc  8806  r1lim  8808  r1ord  8816  r1ord3  8818  jech9.3  8850  onwf  8866  ssrankr1  8871  r1val3  8874  r1pw  8881  rankuni  8899  rankr1b  8900  alephcard  9083  alephnbtwn  9084  alephgeom  9095  dfac3  9134  dfac12lem1  9157  dfac12lem2  9158  cda1dif  9190  cdacomen  9195  cdadom1  9200  cdainf  9206  pwcdadom  9230  ackbij2lem3  9255  cfsmolem  9284  alephsing  9290  fin23lem31  9357  itunisuc  9433  itunitc1  9434  ituniiun  9436  hsmexlem6  9445  zorn2lem4  9513  ttukeylem3  9525  fnct  9551  alephadd  9591  alephreg  9596  pwcfsdom  9597  cfpwsdom  9598  r1limwun  9750  r1wunlim  9751  rankcf  9791  inatsk  9792  r1tskina  9796  grur1  9834  dmaddpi  9904  dmmulpi  9905  genpdm  10016  fsuppmapnn0fiublem  12983  fsuppmapnn0fiub  12984  fsuppmapnn0fiubOLD  12985  hashkf  13313  hashfn  13356  wrdlndm  13507  cshimadifsn  13775  cshimadifsn0  13776  shftfn  14012  rlimi2  14444  bpolylem  14978  phimullem  15686  0rest  16292  restsspw  16294  firest  16295  prdsbas2  16331  prdsplusgval  16335  prdsmulrval  16337  prdsleval  16339  prdsdsval  16340  prdsvscaval  16341  imasleval  16403  xpsfrnel2  16427  homfeqbas  16557  cidpropd  16571  2oppchomf  16585  sscpwex  16676  sscfn1  16678  sscfn2  16679  ssclem  16680  isssc  16681  rescval2  16689  issubc2  16697  cofuval  16743  resfval2  16754  resf1st  16755  resf2nd  16756  funcres  16757  fucbas  16821  fuchom  16822  xpcbas  17019  xpchomfval  17020  xpccofval  17023  oppchofcl  17101  oyoncl  17111  gsumpropd2lem  17474  frmdss2  17601  gicer  17919  psgndmsubg  18122  psgneldm  18123  psgneldm2  18124  psgnval  18127  prdsmgp  18810  lspextmo  19258  psgnghm  20128  psgnghm2  20129  dsmmbas2  20283  dsmmfi  20284  dsmmelbas  20285  frlmsslsp  20337  islindf4  20379  ofco2  20459  cldrcl  21032  iscldtop  21101  neiss2  21107  restrcl  21163  restbas  21164  ssrest  21182  resstopn  21192  ptval  21575  txdis1cn  21640  qtopcld  21718  qtoprest  21722  kqsat  21736  kqdisj  21737  kqcldsat  21738  isr0  21742  kqnrmlem1  21748  kqnrmlem2  21749  hmphtop  21783  hmpher  21789  elfm3  21955  ustn0  22225  nghmfval  22727  isnghm  22728  ovolunlem1  23465  uniiccdif  23546  cpncn  23898  cpnres  23899  ulmf2  24337  tglngne  25644  uhgrn0  26161  upgrfn  26181  upgrex  26186  umgrfn  26193  fnunres1  29724  fcoinver  29725  ofpreima  29774  ofpreima2  29775  mdetpmtr1  30198  ofcfval  30469  probfinmeasb  30800  coinflipspace  30851  bnj564  31121  bnj945  31151  bnj545  31272  bnj548  31274  bnj570  31282  bnj900  31306  bnj929  31313  bnj983  31328  bnj1018  31339  bnj1110  31357  bnj1121  31360  bnj1145  31368  bnj1245  31389  bnj1253  31392  bnj1286  31394  bnj1280  31395  bnj1296  31396  bnj1311  31399  bnj1442  31424  bnj1450  31425  bnj1498  31436  bnj1514  31438  bnj1501  31442  cvmtop1  31549  cvmtop2  31550  dfrdg2  32006  frrlem3  32088  frrlem4  32089  frrlem5e  32094  frrlem11  32098  imageval  32343  filnetlem4  32682  sdclem2  33851  prdstotbnd  33906  heibor1lem  33921  diadm  36826  dibdiadm  36946  dibdmN  36948  dicdmN  36975  dihdm  37060  ismrc  37766  dnnumch3lem  38118  dnnumch3  38119  aomclem4  38129  aomclem6  38131  ntrclsfv1  38855  ntrneifv1  38879  fnchoice  39687  fnresdmss  39847  wessf1ornlem  39870  fndmd  39940  icccncfext  40603  stoweidlem35  40755  stoweidlem59  40779  fnresfnco  41712  fnbrafvb  41740  fnxpdmdm  42278  plusfreseq  42282
  Copyright terms: Public domain W3C validator