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

Theorem fnresdm 5897
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 5886 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 fndm 5887 . . 3 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3 eqimss 3616 . . 3 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
42, 3syl 17 . 2 (𝐹 Fn 𝐴 → dom 𝐹𝐴)
5 relssres 5341 . 2 ((Rel 𝐹 ∧ dom 𝐹𝐴) → (𝐹𝐴) = 𝐹)
61, 4, 5syl2anc 690 1 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3536  dom cdm 5025  cres 5027  Rel wrel 5030   Fn wfn 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pr 4825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-xp 5031  df-rel 5032  df-dm 5035  df-res 5037  df-fun 5789  df-fn 5790
This theorem is referenced by:  fnima  5906  fresin  5968  resasplit  5969  fresaunres2  5971  fvreseq1  6208  fnsnb  6312  fninfp  6320  fnsnsplit  6330  fsnunfv  6333  fsnunres  6334  fnsuppeq0  7184  mapunen  7988  fnfi  8097  canthp1lem2  9328  fseq1p1m1  12235  facnn  12876  fac0  12877  hashgval  12934  hashinf  12936  rlimres  14080  lo1res  14081  rlimresb  14087  isercolllem2  14187  isercoll  14189  ruclem4  14745  fsets  15666  sscres  16249  sscid  16250  gsumzres  18076  pwssplit1  18823  zzngim  19662  ptuncnv  21359  ptcmpfi  21365  tsmsres  21696  imasdsf1olem  21926  tmslem  22035  tmsxms  22039  imasf1oxms  22042  prdsxms  22083  tmsxps  22089  tmsxpsmopn  22090  isngp2  22149  tngngp2  22201  cnfldms  22318  cncms  22873  cnfldcusp  22875  mbfres2  23132  dvres  23395  dvres3a  23398  cpnres  23420  dvmptres3  23439  dvlip2  23476  dvgt0lem2  23484  dvne0  23492  rlimcnp2  24407  jensen  24429  eupath2  26270  sspg  26768  ssps  26770  sspn  26776  hhsssh  27313  fnresin  28615  padct  28688  ffsrn  28695  resf1o  28696  gsumle  28913  cnrrext  29185  indf1ofs  29218  eulerpartlemt  29563  bnj142OLD  29851  subfacp1lem3  30221  subfacp1lem5  30223  cvmliftlem11  30334  poimirlem9  32388  mapfzcons1  36098  eq0rabdioph  36158  eldioph4b  36193  diophren  36195  pwssplit4  36477  dvresntr  38607  sge0split  39103  eupthvdres  41402
  Copyright terms: Public domain W3C validator