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

Theorem fndm 5507
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 5418 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 461 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   dom cdm 4836   Fun wfun 5409    Fn wfn 5410
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 5418
This theorem is referenced by:  funfni  5508  fndmu  5509  fnbr  5510  fnco  5516  fnresdm  5517  fnresdisj  5518  fnssresb  5520  fn0  5527  fnimadisj  5528  fnimaeq0  5529  dmmpti  5537  fdm  5560  f1dm  5607  f1odm  5642  f1o00  5670  fvelimab  5744  fvun1  5759  eqfnfv2  5795  fndmdif  5804  fneqeql2  5809  elpreima  5820  fsn2  5880  fnprb  5933  fnprOLD  5934  fconst3  5938  fconst4  5939  fnfvima  5952  fnunirn  5967  dff13  5968  nvof1o  5984  f1eqcocnv  5996  oprssov  6231  offval  6326  ofrfval  6327  fnexALT  6542  dmmpt2  6643  dmmpt2ga  6644  curry1  6663  curry1val  6664  curry2  6666  curry2val  6668  fparlem3  6673  fparlem4  6674  fnwelem  6686  suppvalfn  6696  suppfnss  6713  fnsuppres  6715  tposfo2  6767  smodm2  6812  smoel2  6820  tfrlem5  6835  tfrlem8  6839  tfrlem9  6840  tfrlem9a  6841  tfrlem13  6845  tfr2  6853  tz7.44-2  6859  tz7.44-3  6860  rdgsuc  6876  rdglim  6878  frsucmptn  6890  tz7.48-2  6893  tz7.48-1  6894  tz7.48-3  6895  tz7.49  6896  brwitnlem  6943  om0x  6955  oaabs2  7080  omabs  7082  elpmi  7227  elmapex  7229  pmresg  7236  pmsspw  7243  ixpprc  7280  undifixp  7295  bren  7315  fndmeng  7382  wemapso  7761  ixpiunwdom  7802  inf0  7823  noinfepOLD  7862  r1suc  7973  r1lim  7975  r1ord  7983  r1ord3  7985  jech9.3  8017  onwf  8033  ssrankr1  8038  r1val3  8041  r1pw  8048  rankuni  8066  rankr1b  8067  alephcard  8236  alephnbtwn  8237  alephgeom  8248  dfac3  8287  dfac12lem1  8308  dfac12lem2  8309  cda1dif  8341  cdacomen  8346  cdadom1  8351  cdainf  8357  pwcdadom  8381  ackbij2lem3  8406  cfsmolem  8435  alephsing  8441  fin23lem31  8508  itunisuc  8584  itunitc1  8585  ituniiun  8587  hsmexlem6  8596  zorn2lem4  8664  ttukeylem3  8676  alephadd  8737  alephreg  8742  pwcfsdom  8743  cfpwsdom  8744  r1limwun  8899  r1wunlim  8900  rankcf  8940  inatsk  8941  r1tskina  8945  grur1  8983  dmaddpi  9055  dmmulpi  9056  genpdm  9167  hashkf  12101  hashfn  12134  shftfn  12558  rlimi2  12988  rlimmptrcl  13081  phimullem  13850  0rest  14364  restsspw  14366  firest  14367  prdsbas2  14403  prdsplusgval  14407  prdsmulrval  14409  prdsleval  14411  prdsdsval  14412  prdsvscaval  14413  imasleval  14475  xpsfrnel2  14499  homfeqbas  14631  cidpropd  14645  2oppchomf  14659  sscpwex  14724  sscfn1  14726  sscfn2  14727  ssclem  14728  isssc  14729  rescval2  14737  issubc2  14745  cofuval  14788  resfval2  14799  resf1st  14800  resf2nd  14801  funcres  14802  fucbas  14866  fuchom  14867  xpcbas  14984  xpchomfval  14985  xpccofval  14988  oppchofcl  15066  oyoncl  15076  frmdss2  15534  gicer  15797  psgndmsubg  16001  psgneldm  16002  psgneldm2  16003  psgnval  16006  prdsmgp  16692  lspextmo  17115  psgnghm  17969  psgnghm2  17970  dsmmbas2  18121  dsmmfi  18122  dsmmelbas  18123  frlmsslsp  18182  frlmsslspOLD  18183  islindf4  18226  ofco2  18291  cldrcl  18589  iscldtop  18658  neiss2  18664  restrcl  18720  restbas  18721  ssrest  18739  resstopn  18749  ptval  19102  txdis1cn  19167  qtopcld  19245  qtoprest  19249  kqsat  19263  kqdisj  19264  kqcldsat  19265  isr0  19269  kqnrmlem1  19275  kqnrmlem2  19276  hmphtop  19310  hmpher  19316  elfm3  19482  ustn0  19754  nghmfval  20260  isnghm  20261  ovolunlem1  20939  uniiccdif  21017  iblcnlem  21225  cpncn  21369  cpnres  21370  dvmptres3  21389  ulmf2  21808  tglngne  22942  uhgraun  23180  umgraf  23187  vdgrfval  23500  eupai  23523  eupap1  23532  ghablo  23791  ofpreima  25919  ofpreima2  25920  fnct  25948  gsumpropd2lem  26177  ofcfval  26476  sseqf  26705  probfinmeasb  26742  coinflipspace  26793  cvmtop1  27079  cvmtop2  27080  dfrdg2  27538  wfrlem3  27655  wfrlem4  27656  wfrlem9  27661  wfrlem12  27664  frrlem3  27699  frrlem4  27700  frrlem5e  27705  frrlem11  27709  imageval  27890  bpolylem  28120  filnetlem4  28527  sdclem2  28563  prdstotbnd  28618  heibor1lem  28633  ismrc  28962  dnnumch3lem  29324  dnnumch3  29325  aomclem4  29335  aomclem6  29337  fnchoice  29676  stoweidlem35  29755  stoweidlem59  29779  fnresfnco  29957  fnbrafvb  29985  bnj564  31570  bnj945  31601  bnj545  31722  bnj548  31724  bnj570  31732  bnj900  31756  bnj929  31763  bnj983  31778  bnj1018  31789  bnj1110  31807  bnj1121  31810  bnj1145  31818  bnj1245  31839  bnj1253  31842  bnj1286  31844  bnj1280  31845  bnj1296  31846  bnj1311  31849  bnj1442  31874  bnj1450  31875  bnj1498  31886  bnj1514  31888  bnj1501  31892  diadm  34402  dibdiadm  34522  dibdmN  34524  dicdmN  34551  dihdm  34636
  Copyright terms: Public domain W3C validator