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

Theorem fnresdm 6460
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 6448 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 fndm 6449 . . 3 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3 eqimss 4022 . . 3 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
42, 3syl 17 . 2 (𝐹 Fn 𝐴 → dom 𝐹𝐴)
5 relssres 5887 . 2 ((Rel 𝐹 ∧ dom 𝐹𝐴) → (𝐹𝐴) = 𝐹)
61, 4, 5syl2anc 584 1 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wss 3935  dom cdm 5549  cres 5551  Rel wrel 5554   Fn wfn 6344
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 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-xp 5555  df-rel 5556  df-dm 5559  df-res 5561  df-fun 6351  df-fn 6352
This theorem is referenced by:  fnima  6472  fresin  6541  resasplit  6542  fresaunres2  6544  fvreseq1  6802  fnsnr  6920  fninfp  6929  fnsnsplit  6939  fsnunfv  6942  fsnunres  6943  fnsuppeq0  7849  mapunen  8675  fnfi  8785  canthp1lem2  10064  fseq1p1m1  12971  facnn  13625  fac0  13626  hashgval  13683  hashinf  13685  rlimres  14905  lo1res  14906  rlimresb  14912  isercolllem2  15012  isercoll  15014  ruclem4  15577  fsets  16506  sscres  17083  sscid  17084  gsumzres  18960  rnrhmsubrg  19498  pwssplit1  19762  zzngim  20629  ptuncnv  22345  ptcmpfi  22351  tsmsres  22681  imasdsf1olem  22912  tmslem  23021  tmsxms  23025  imasf1oxms  23028  prdsxms  23069  tmsxps  23075  tmsxpsmopn  23076  isngp2  23135  tngngp2  23190  cnfldms  23313  cncms  23887  cnfldcusp  23889  mbfres2  24175  dvres  24438  dvres3a  24441  cpnres  24463  dvmptres3  24482  dvlip2  24521  dvgt0lem2  24529  dvne0  24537  rlimcnp2  25472  jensen  25494  eupthvdres  27942  sspg  28433  ssps  28435  sspn  28441  hhsssh  28974  fnresin  30300  padct  30382  ffsrn  30392  resf1o  30393  gsumle  30653  symgcom  30655  cycpmconjvlem  30711  cycpmconjslem1  30724  cnrrext  31151  indf1ofs  31185  eulerpartlemt  31529  subfacp1lem3  32327  subfacp1lem5  32329  cvmliftlem11  32440  poimirlem9  34783  mapfzcons1  39194  eq0rabdioph  39253  eldioph4b  39288  diophren  39290  pwssplit4  39569  dvresntr  42082  sge0split  42572
  Copyright terms: Public domain W3C validator