Theorem fnresdm 6609

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

Step	Hyp	Ref	Expression
1		fnrel 6592	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6593	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3990	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5979	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 584	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3899  dom cdm 5622   ↾ cres 5624  Rel wrel 5627   Fn wfn 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629  df-dm 5632  df-res 5634  df-fun 6492  df-fn 6493

This theorem is referenced by:  fnima  6620  fresin  6701  resasplit  6702  fresaunres2  6704  fvreseq1  6982  fnsnr  7107  fninfp  7118  fnsnsplit  7128  fsnunfv  7131  fsnunres  7132  fnsuppeq0  8132  mapunen  9072  dif1enlem  9082  fnfi  9100  canthp1lem2  10562  fseq1p1m1  13512  facnn  14196  fac0  14197  hashgval  14254  hashinf  14256  rlimres  15479  lo1res  15480  rlimresb  15486  isercolllem2  15587  isercoll  15589  ruclem4  16157  fsets  17094  sscres  17745  sscid  17746  gsumzres  19836  gsumle  20072  pwssplit1  21009  zzngim  21505  ptuncnv  23749  ptcmpfi  23755  tsmsres  24086  imasdsf1olem  24315  tmslem  24424  tmsxms  24428  imasf1oxms  24431  prdsxms  24472  tmsxps  24478  tmsxpsmopn  24479  isngp2  24539  tngngp2  24594  cnfldms  24717  cncms  25309  cnfldcusp  25311  mbfres2  25600  dvres  25866  dvres3a  25869  cpnres  25893  dvmptres3  25914  dvlip2  25954  dvgt0lem2  25962  dvne0  25970  rlimcnp2  26930  jensen  26953  eupthvdres  30259  sspg  30752  ssps  30754  sspn  30760  hhsssh  31293  fnresin  32651  padct  32746  ffsrn  32756  resf1o  32758  indf1ofs  32897  symgcom  33114  cycpmconjvlem  33172  cycpmconjslem1  33185  nsgqusf1o  33446  ply1degltdimlem  33728  cnrrext  34116  eulerpartlemt  34477  subfacp1lem3  35325  subfacp1lem5  35327  cvmliftlem11  35438  poimirlem9  37769  dvun  42556  mapfzcons1  42901  eq0rabdioph  42960  eldioph4b  42995  diophren  42997  pwssplit4  43273  tfsconcatrev  43532  dvresntr  46104  sge0split  46595  imaidfu2  49298