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

Theorem fndm 6449
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 6352 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 497 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  dom cdm 5549  Fun wfun 6343   Fn wfn 6344
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 208  df-an 397  df-fn 6352
This theorem is referenced by:  fndmd  6450  funfni  6451  fndmu  6452  fnbr  6453  fnco  6459  fnresdm  6460  fnresdisj  6461  fnssresb  6463  fn0  6473  fnimadisj  6474  fnimaeq0  6475  dmmpti  6486  fdm  6516  f1dm  6573  f1odm  6613  fvelimab  6731  fvun1  6748  eqfnfv2  6796  fndmdif  6805  fneqeql2  6810  elpreima  6821  fsn2  6891  fnprb  6963  fntpb  6964  fconst3  6968  fconst4  6969  fnfvima  6986  fnunirn  7003  dff13  7004  nvof1o  7028  f1eqcocnv  7048  oprssov  7306  fnexALT  7643  dmmpo  7760  dmmpoga  7762  curry1  7790  curry1val  7791  curry2  7793  curry2val  7795  fparlem3  7800  fparlem4  7801  offsplitfpar  7806  fnwelem  7816  suppvalfn  7828  suppfnss  7846  fnsuppres  7848  tposfo2  7906  wfrlem3  7947  wfrlem4  7949  wfrdmcl  7954  wfrlem12  7957  wfrlem17  7962  smodm2  7983  smoel2  7991  tfrlem5  8007  tfrlem8  8011  tfrlem9  8012  tfrlem9a  8013  tfrlem13  8017  tfr2  8025  tz7.44-2  8034  tz7.44-3  8035  rdgsuc  8051  rdglim  8053  frsucmptn  8065  tz7.48-2  8069  tz7.48-1  8070  tz7.48-3  8071  tz7.49  8072  brwitnlem  8123  om0x  8135  oaabs2  8262  omabs  8264  elpmi  8415  elmapex  8417  pmresg  8424  pmsspw  8431  ixpprc  8472  undifixp  8487  bren  8507  fndmeng  8576  ixpiunwdom  9044  inf0  9073  r1suc  9188  r1lim  9190  r1ord  9198  r1ord3  9200  jech9.3  9232  onwf  9248  ssrankr1  9253  r1val3  9256  r1pw  9263  rankuni  9281  rankr1b  9282  alephcard  9485  alephnbtwn  9486  alephgeom  9497  dfac3  9536  dfac12lem1  9558  dfac12lem2  9559  ackbij2lem3  9652  cfsmolem  9681  alephsing  9687  fin23lem31  9754  itunisuc  9830  itunitc1  9831  ituniiun  9833  hsmexlem6  9842  zorn2lem4  9910  ttukeylem3  9922  fnct  9948  alephadd  9988  alephreg  9993  pwcfsdom  9994  cfpwsdom  9995  r1limwun  10147  r1wunlim  10148  rankcf  10188  inatsk  10189  r1tskina  10193  grur1  10231  dmaddpi  10301  dmmulpi  10302  genpdm  10413  fsuppmapnn0fiublem  13348  fsuppmapnn0fiub  13349  seqexw  13375  hashkf  13682  hashfn  13726  wrdlndmOLD  13870  cshimadifsn  14181  cshimadifsn0  14182  shftfn  14422  rlimi2  14861  bpolylem  15392  phimullem  16106  0rest  16693  restsspw  16695  firest  16696  prdsbas2  16732  prdsplusgval  16736  prdsmulrval  16738  prdsleval  16740  prdsdsval  16741  prdsvscaval  16742  imasleval  16804  fnpr2ob  16821  homfeqbas  16956  cidpropd  16970  2oppchomf  16984  sscpwex  17075  sscfn1  17077  sscfn2  17078  ssclem  17079  isssc  17080  rescval2  17088  issubc2  17096  cofuval  17142  resfval2  17153  resf1st  17154  resf2nd  17155  funcres  17156  fucbas  17220  fuchom  17221  xpcbas  17418  xpchomfval  17419  xpccofval  17422  oppchofcl  17500  oyoncl  17510  gsumpropd2lem  17879  mulgfval  18166  gicer  18356  psgndmsubg  18561  psgneldm  18562  psgneldm2  18563  psgnval  18566  prdsmgp  19291  lspextmo  19759  psgnghm  20654  psgnghm2  20655  dsmmbas2  20811  dsmmfi  20812  dsmmelbas  20813  islindf4  20912  ofco2  20990  cldrcl  21564  iscldtop  21633  neiss2  21639  restrcl  21695  restbas  21696  ssrest  21714  resstopn  21724  ptval  22108  txdis1cn  22173  qtopcld  22251  qtoprest  22255  kqsat  22269  kqdisj  22270  kqcldsat  22271  isr0  22275  kqnrmlem1  22281  kqnrmlem2  22282  hmphtop  22316  hmpher  22322  elfm3  22488  ustn0  22758  nghmfval  23260  isnghm  23261  ovolunlem1  24027  uniiccdif  24108  cpncn  24462  cpnres  24463  ulmf2  24901  tglngne  26264  uhgrn0  26780  upgrfn  26800  upgrex  26805  umgrfn  26812  fnunres1  30285  fcoinver  30286  nfpconfp  30306  ofpreima  30339  ofpreima2  30340  fnpreimac  30345  mdetpmtr1  30988  probfinmeasb  31586  coinflipspace  31638  bnj564  31915  bnj945  31945  bnj545  32067  bnj548  32069  bnj570  32077  bnj900  32101  bnj929  32108  bnj983  32123  bnj1018  32134  bnj1110  32152  bnj1145  32163  bnj1245  32184  bnj1253  32187  bnj1286  32189  bnj1280  32190  bnj1296  32191  bnj1311  32194  bnj1442  32219  bnj1450  32220  bnj1498  32231  bnj1514  32233  bnj1501  32237  cvmtop1  32405  cvmtop2  32406  dfrdg2  32938  frrlem3  33023  frrlem4  33024  frrlem8  33028  frrlem10  33030  imageval  33289  filnetlem4  33627  sdclem2  34900  prdstotbnd  34955  heibor1lem  34970  dibdiadm  38173  dibdmN  38175  dicdmN  38202  dihdm  38287  fnsnbt  39000  ismrc  39178  dnnumch3lem  39526  dnnumch3  39527  aomclem4  39537  aomclem6  39539  ntrclsfv1  40285  ntrneifv1  40309  grur1cld  40448  fnresdmss  41304  icccncfext  42050  stoweidlem35  42201  stoweidlem59  42225  fnresfnco  43157  fnbrafvb  43234  fnxpdmdm  43882  plusfreseq  43886
  Copyright terms: Public domain W3C validator