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

Theorem fnresdm 6459
Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
Assertion
Ref Expression
fnresdm (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)

Proof of Theorem fnresdm
StepHypRef Expression
1 fnrel 6447 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 fndm 6448 . . 3 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3 eqimss 4020 . . 3 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
42, 3syl 17 . 2 (𝐹 Fn 𝐴 → dom 𝐹𝐴)
5 relssres 5886 . 2 ((Rel 𝐹 ∧ dom 𝐹𝐴) → (𝐹𝐴) = 𝐹)
61, 4, 5syl2anc 584 1 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3933  dom cdm 5548  cres 5550  Rel wrel 5553   Fn wfn 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-dm 5558  df-res 5560  df-fun 6350  df-fn 6351
This theorem is referenced by:  fnima  6471  fresin  6540  resasplit  6541  fresaunres2  6543  fvreseq1  6801  fnsnr  6919  fninfp  6928  fnsnsplit  6938  fsnunfv  6941  fsnunres  6942  fnsuppeq0  7847  mapunen  8674  fnfi  8784  canthp1lem2  10063  fseq1p1m1  12969  facnn  13623  fac0  13624  hashgval  13681  hashinf  13683  rlimres  14903  lo1res  14904  rlimresb  14910  isercolllem2  15010  isercoll  15012  ruclem4  15575  fsets  16504  sscres  17081  sscid  17082  gsumzres  18958  rnrhmsubrg  19496  pwssplit1  19760  zzngim  20627  ptuncnv  22343  ptcmpfi  22349  tsmsres  22679  imasdsf1olem  22910  tmslem  23019  tmsxms  23023  imasf1oxms  23026  prdsxms  23067  tmsxps  23073  tmsxpsmopn  23074  isngp2  23133  tngngp2  23188  cnfldms  23311  cncms  23885  cnfldcusp  23887  mbfres2  24173  dvres  24436  dvres3a  24439  cpnres  24461  dvmptres3  24480  dvlip2  24519  dvgt0lem2  24527  dvne0  24535  rlimcnp2  25471  jensen  25493  eupthvdres  27941  sspg  28432  ssps  28434  sspn  28440  hhsssh  28973  fnresin  30299  padct  30381  ffsrn  30391  resf1o  30392  gsumle  30652  symgcom  30654  cycpmconjvlem  30710  cycpmconjslem1  30723  cnrrext  31150  indf1ofs  31184  eulerpartlemt  31528  subfacp1lem3  32326  subfacp1lem5  32328  cvmliftlem11  32439  poimirlem9  34782  mapfzcons1  39192  eq0rabdioph  39251  eldioph4b  39286  diophren  39288  pwssplit4  39567  dvresntr  42078  sge0split  42568
  Copyright terms: Public domain W3C validator