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

Theorem fndm 5522
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm  |-  ( F  Fn  A  ->  dom  F  =  A )

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5433 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 464 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   dom cdm 4852   Fun wfun 5424    Fn wfn 5425
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 185  df-an 371  df-fn 5433
This theorem is referenced by:  funfni  5523  fndmu  5524  fnbr  5525  fnco  5531  fnresdm  5532  fnresdisj  5533  fnssresb  5535  fn0  5542  fnimadisj  5543  fnimaeq0  5544  dmmpti  5552  fdm  5575  f1dm  5622  f1odm  5657  f1o00  5685  fvelimab  5759  fvun1  5774  eqfnfv2  5810  fndmdif  5819  fneqeql2  5824  elpreima  5835  fsn2  5895  fnprb  5948  fnprOLD  5949  fconst3  5953  fconst4  5954  fnfvima  5967  fnunirn  5982  dff13  5983  nvof1o  5999  f1eqcocnv  6011  oprssov  6244  offval  6339  ofrfval  6340  fnexALT  6555  dmmpt2  6656  dmmpt2ga  6657  curry1  6676  curry1val  6677  curry2  6679  curry2val  6681  fparlem3  6686  fparlem4  6687  fnwelem  6699  suppvalfn  6709  suppfnss  6726  fnsuppres  6728  tposfo2  6780  smodm2  6828  smoel2  6836  tfrlem5  6851  tfrlem8  6855  tfrlem9  6856  tfrlem9a  6857  tfrlem13  6861  tfr2  6869  tz7.44-2  6875  tz7.44-3  6876  rdgsuc  6892  rdglim  6894  frsucmptn  6906  tz7.48-2  6909  tz7.48-1  6910  tz7.48-3  6911  tz7.49  6912  brwitnlem  6959  om0x  6971  oaabs2  7096  omabs  7098  elpmi  7243  elmapex  7245  pmresg  7252  pmsspw  7259  ixpprc  7296  undifixp  7311  bren  7331  fndmeng  7398  wemapso  7777  ixpiunwdom  7818  inf0  7839  noinfepOLD  7878  r1suc  7989  r1lim  7991  r1ord  7999  r1ord3  8001  jech9.3  8033  onwf  8049  ssrankr1  8054  r1val3  8057  r1pw  8064  rankuni  8082  rankr1b  8083  alephcard  8252  alephnbtwn  8253  alephgeom  8264  dfac3  8303  dfac12lem1  8324  dfac12lem2  8325  cda1dif  8357  cdacomen  8362  cdadom1  8367  cdainf  8373  pwcdadom  8397  ackbij2lem3  8422  cfsmolem  8451  alephsing  8457  fin23lem31  8524  itunisuc  8600  itunitc1  8601  ituniiun  8603  hsmexlem6  8612  zorn2lem4  8680  ttukeylem3  8692  alephadd  8753  alephreg  8758  pwcfsdom  8759  cfpwsdom  8760  r1limwun  8915  r1wunlim  8916  rankcf  8956  inatsk  8957  r1tskina  8961  grur1  8999  dmaddpi  9071  dmmulpi  9072  genpdm  9183  hashkf  12117  hashfn  12150  shftfn  12574  rlimi2  13004  rlimmptrcl  13097  phimullem  13866  0rest  14380  restsspw  14382  firest  14383  prdsbas2  14419  prdsplusgval  14423  prdsmulrval  14425  prdsleval  14427  prdsdsval  14428  prdsvscaval  14429  imasleval  14491  xpsfrnel2  14515  homfeqbas  14647  cidpropd  14661  2oppchomf  14675  sscpwex  14740  sscfn1  14742  sscfn2  14743  ssclem  14744  isssc  14745  rescval2  14753  issubc2  14761  cofuval  14804  resfval2  14815  resf1st  14816  resf2nd  14817  funcres  14818  fucbas  14882  fuchom  14883  xpcbas  15000  xpchomfval  15001  xpccofval  15004  oppchofcl  15082  oyoncl  15092  gsumpropd2lem  15517  frmdss2  15553  gicer  15816  psgndmsubg  16020  psgneldm  16021  psgneldm2  16022  psgnval  16025  prdsmgp  16714  lspextmo  17149  psgnghm  18022  psgnghm2  18023  dsmmbas2  18174  dsmmfi  18175  dsmmelbas  18176  frlmsslsp  18235  frlmsslspOLD  18236  islindf4  18279  ofco2  18344  cldrcl  18642  iscldtop  18711  neiss2  18717  restrcl  18773  restbas  18774  ssrest  18792  resstopn  18802  ptval  19155  txdis1cn  19220  qtopcld  19298  qtoprest  19302  kqsat  19316  kqdisj  19317  kqcldsat  19318  isr0  19322  kqnrmlem1  19328  kqnrmlem2  19329  hmphtop  19363  hmpher  19369  elfm3  19535  ustn0  19807  nghmfval  20313  isnghm  20314  ovolunlem1  20992  uniiccdif  21070  iblcnlem  21278  cpncn  21422  cpnres  21423  dvmptres3  21442  ulmf2  21861  tglngne  22996  uhgraun  23257  umgraf  23264  vdgrfval  23577  eupai  23600  eupap1  23609  ghablo  23868  ofpreima  25996  ofpreima2  25997  fnct  26025  ofcfval  26552  sseqf  26787  probfinmeasb  26824  coinflipspace  26875  cvmtop1  27161  cvmtop2  27162  dfrdg2  27621  wfrlem3  27738  wfrlem4  27739  wfrlem9  27744  wfrlem12  27747  frrlem3  27782  frrlem4  27783  frrlem5e  27788  frrlem11  27792  imageval  27973  bpolylem  28203  filnetlem4  28614  sdclem2  28650  prdstotbnd  28705  heibor1lem  28720  ismrc  29049  dnnumch3lem  29411  dnnumch3  29412  aomclem4  29422  aomclem6  29424  fnchoice  29763  stoweidlem35  29842  stoweidlem59  29866  fnresfnco  30044  fnbrafvb  30072  fsuppmapnn0fiublem  30810  fsuppmapnn0fiub  30811  bnj564  31748  bnj945  31779  bnj545  31900  bnj548  31902  bnj570  31910  bnj900  31934  bnj929  31941  bnj983  31956  bnj1018  31967  bnj1110  31985  bnj1121  31988  bnj1145  31996  bnj1245  32017  bnj1253  32020  bnj1286  32022  bnj1280  32023  bnj1296  32024  bnj1311  32027  bnj1442  32052  bnj1450  32053  bnj1498  32064  bnj1514  32066  bnj1501  32070  diadm  34692  dibdiadm  34812  dibdmN  34814  dicdmN  34841  dihdm  34926
  Copyright terms: Public domain W3C validator