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

Theorem fnresdm 6620
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 6604 . 2 (𝐹 Fn 𝐴 → Rel 𝐹)
2 fndm 6605 . . 3 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3 eqimss 4000 . . 3 (dom 𝐹 = 𝐴 → dom 𝐹𝐴)
42, 3syl 17 . 2 (𝐹 Fn 𝐴 → dom 𝐹𝐴)
5 relssres 5978 . 2 ((Rel 𝐹 ∧ dom 𝐹𝐴) → (𝐹𝐴) = 𝐹)
61, 4, 5syl2anc 584 1 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wss 3910  dom cdm 5633  cres 5635  Rel wrel 5638   Fn wfn 6491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-xp 5639  df-rel 5640  df-dm 5643  df-res 5645  df-fun 6498  df-fn 6499
This theorem is referenced by:  fnima  6631  fresin  6711  resasplit  6712  fresaunres2  6714  fvreseq1  6989  fnsnr  7111  fninfp  7120  fnsnsplit  7130  fsnunfv  7133  fsnunres  7134  fnsuppeq0  8123  mapunen  9090  dif1enlem  9100  dif1enlemOLD  9101  fnfi  9125  canthp1lem2  10589  fseq1p1m1  13515  facnn  14175  fac0  14176  hashgval  14233  hashinf  14235  rlimres  15440  lo1res  15441  rlimresb  15447  isercolllem2  15550  isercoll  15552  ruclem4  16116  fsets  17041  sscres  17706  sscid  17707  gsumzres  19686  rnrhmsubrg  20254  pwssplit1  20520  zzngim  20959  ptuncnv  23158  ptcmpfi  23164  tsmsres  23495  imasdsf1olem  23726  tmslem  23837  tmslemOLD  23838  tmsxms  23842  imasf1oxms  23845  prdsxms  23886  tmsxps  23892  tmsxpsmopn  23893  isngp2  23953  tngngp2  24016  cnfldms  24139  cncms  24719  cnfldcusp  24721  mbfres2  25009  dvres  25275  dvres3a  25278  cpnres  25301  dvmptres3  25320  dvlip2  25359  dvgt0lem2  25367  dvne0  25375  rlimcnp2  26316  jensen  26338  eupthvdres  29179  sspg  29670  ssps  29672  sspn  29678  hhsssh  30211  fnresin  31540  padct  31636  ffsrn  31646  resf1o  31647  gsumle  31932  symgcom  31934  cycpmconjvlem  31990  cycpmconjslem1  32003  nsgqusf1o  32194  cnrrext  32591  indf1ofs  32625  eulerpartlemt  32971  subfacp1lem3  33776  subfacp1lem5  33778  cvmliftlem11  33889  poimirlem9  36087  mapfzcons1  41026  eq0rabdioph  41085  eldioph4b  41120  diophren  41122  pwssplit4  41402  dvresntr  44149  sge0split  44640
  Copyright terms: Public domain W3C validator