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

Theorem fnresdm 5494
Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
Assertion
Ref Expression
fnresdm  |-  ( F  Fn  A  ->  ( F  |`  A )  =  F )

Proof of Theorem fnresdm
StepHypRef Expression
1 fnrel 5483 . 2  |-  ( F  Fn  A  ->  Rel  F )
2 fndm 5484 . . 3  |-  ( F  Fn  A  ->  dom  F  =  A )
3 eqimss 3343 . . 3  |-  ( dom 
F  =  A  ->  dom  F  C_  A )
42, 3syl 16 . 2  |-  ( F  Fn  A  ->  dom  F 
C_  A )
5 relssres 5123 . 2  |-  ( ( Rel  F  /\  dom  F 
C_  A )  -> 
( F  |`  A )  =  F )
61, 4, 5syl2anc 643 1  |-  ( F  Fn  A  ->  ( F  |`  A )  =  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3263   dom cdm 4818    |` cres 4820   Rel wrel 4823    Fn wfn 5389
This theorem is referenced by:  fnima  5503  fresin  5552  resasplit  5553  fresaunres2  5555  fnsnsplit  5869  fsnunfv  5872  fsnunres  5873  fnsuppeq0  5892  abianfp  6652  mapunen  7212  fnfi  7320  canthp1lem2  8461  fseq1p1m1  11052  facnn  11495  fac0  11496  hashgval  11548  hashinf  11550  rlimres  12279  lo1res  12280  rlimresb  12286  isercolllem2  12386  isercoll  12388  ruclem4  12760  sscres  13950  sscid  13951  gsumzres  15444  zzngim  16756  ptuncnv  17760  ptcmpfi  17766  tsmsres  18094  imasdsf1olem  18311  tmslem  18402  tmsxms  18406  imasf1oxms  18409  prdsxms  18450  tmsxps  18456  tmsxpsmopn  18457  isngp2  18515  tngngp2  18564  cnfldms  18681  cncms  19176  cnfldcusp  19178  mbfres2  19404  dvres  19665  dvres3a  19668  cpnres  19690  dvmptres3  19709  dvlip2  19746  dvgt0lem2  19754  dvne0  19762  rlimcnp2  20672  jensen  20694  eupath2  21550  subgores  21740  sspg  22075  ssps  22077  sspn  22083  hhsssh  22617  indf1ofs  24219  subfacp1lem3  24647  subfacp1lem5  24649  cvmliftlem11  24761  fninfp  26426  mapfzcons1  26464  eq0rabdioph  26526  eldioph4b  26563  diophren  26565  pwssplit1  26857  pwssplit4  26860  bnj142  28431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825  df-dm 4828  df-res 4830  df-fun 5396  df-fn 5397
  Copyright terms: Public domain W3C validator