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

Theorem fnresdm 5914
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 5903 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 fndm 5904 . . 3 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3 eqimss 3620 . . 3 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
42, 3syl 17 . 2 (𝐹 Fn 𝐴 → dom 𝐹𝐴)
5 relssres 5357 . 2 ((Rel 𝐹 ∧ dom 𝐹𝐴) → (𝐹𝐴) = 𝐹)
61, 4, 5syl2anc 691 1 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540  dom cdm 5038  cres 5040  Rel wrel 5043   Fn wfn 5799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-dm 5048  df-res 5050  df-fun 5806  df-fn 5807
This theorem is referenced by:  fnima  5923  fresin  5986  resasplit  5987  fresaunres2  5989  fvreseq1  6226  fnsnb  6337  fninfp  6345  fnsnsplit  6355  fsnunfv  6358  fsnunres  6359  fnsuppeq0  7210  mapunen  8014  fnfi  8123  canthp1lem2  9354  fseq1p1m1  12283  facnn  12924  fac0  12925  hashgval  12982  hashinf  12984  rlimres  14137  lo1res  14138  rlimresb  14144  isercolllem2  14244  isercoll  14246  ruclem4  14802  fsets  15723  sscres  16306  sscid  16307  gsumzres  18133  pwssplit1  18880  zzngim  19720  ptuncnv  21420  ptcmpfi  21426  tsmsres  21757  imasdsf1olem  21988  tmslem  22097  tmsxms  22101  imasf1oxms  22104  prdsxms  22145  tmsxps  22151  tmsxpsmopn  22152  isngp2  22211  tngngp2  22266  cnfldms  22389  cncms  22959  cnfldcusp  22961  mbfres2  23218  dvres  23481  dvres3a  23484  cpnres  23506  dvmptres3  23525  dvlip2  23562  dvgt0lem2  23570  dvne0  23578  rlimcnp2  24493  jensen  24515  eupath2  26507  sspg  26967  ssps  26969  sspn  26975  hhsssh  27510  fnresin  28812  padct  28885  ffsrn  28892  resf1o  28893  gsumle  29110  cnrrext  29382  indf1ofs  29415  eulerpartlemt  29760  bnj142OLD  30048  subfacp1lem3  30418  subfacp1lem5  30420  cvmliftlem11  30531  poimirlem9  32588  mapfzcons1  36298  eq0rabdioph  36358  eldioph4b  36393  diophren  36395  pwssplit4  36677  dvresntr  38806  sge0split  39302  eupthvdres  41403
  Copyright terms: Public domain W3C validator