Theorem fnresdm 6651

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 6634	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6635	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3989	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 18	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6015	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 596	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899  dom cdm 5655   ↾ cres 5657  Rel wrel 5660   Fn wfn 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-dm 5665  df-res 5667  df-fun 6535  df-fn 6536

This theorem is used by:  fnima  6662  fresin  6744  resasplit  6745  fresaunres2  6747  fvreseq1  7031  fnsnr  7161  fninfp  7172  fnsnsplit  7182  fsnunfv  7185  fsnunres  7186  fnsuppeq0  8190  mapunen  9144  dif1enlem  9154  fnfi  9172  canthp1lem2  10662  fseq1p1m1  13653  facnn  14339  fac0  14340  hashgval  14397  hashinf  14399  rlimres  15645  lo1res  15646  rlimresb  15652  isercolllem2  15753  isercoll  15755  ruclem4  16322  fsets  17261  sscres  17912  sscid  17913  gsumzres  20036  gsumle  20272  pwssplit1  21243  zzngim  21765  ptuncnv  24033  ptcmpfi  24039  tsmsres  24370  imasdsf1olem  24599  tmslem  24708  tmsxms  24712  imasf1oxms  24715  prdsxms  24756  tmsxps  24762  tmsxpsmopn  24763  isngp2  24823  tngngp2  24878  cnfldms  25001  cncms  25583  cnfldcusp  25585  mbfres2  25873  dvres  26138  dvres3a  26141  cpnres  26164  dvmptres3  26183  dvlip2  26222  dvgt0lem2  26230  dvne0  26238  rlimcnp2  27203  jensen  27225  eupthvdres  30715  sspg  31209  ssps  31211  sspn  31217  hhsssh  31750  fnresin  33097  padct  33189  ffsrn  33199  resf1o  33201  indf1ofs  33312  symgcom  33523  cycpmconjvlem  33581  cycpmconjslem1  33594  nsgqusf1o  33845  ply1degltdimlem  34132  cnrrext  34520  eulerpartlemt  34882  subfacp1lem3  35761  subfacp1lem5  35763  cvmliftlem11  35874  poimirlem9  38378  dvun  43234  mapfzcons1  43562  eq0rabdioph  43621  eldioph4b  43652  diophren  43654  pwssplit4  43930  tfsconcatrev  44189  dvresntr  46746  sge0split  47237  imaidfu2  50037