Theorem fnresdm 6658

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906  dom cdm 5663   ↾ cres 5665  Rel wrel 5668   Fn wfn 6535

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670  df-dm 5673  df-res 5675  df-fun 6542  df-fn 6543

This theorem is used by:  fnima  6669  fresin  6751  resasplit  6752  fresaunres2  6754  fvreseq1  7038  fnsnr  7167  fninfp  7178  fnsnsplit  7188  fsnunfv  7191  fsnunres  7192  fnsuppeq0  8194  mapunen  9141  dif1enlem  9151  fnfi  9169  canthp1lem2  10653  fseq1p1m1  13643  facnn  14329  fac0  14330  hashgval  14387  hashinf  14389  rlimres  15633  lo1res  15634  rlimresb  15640  isercolllem2  15741  isercoll  15743  ruclem4  16312  fsets  17251  sscres  17902  sscid  17903  gsumzres  20023  gsumle  20259  pwssplit1  21230  zzngim  21752  ptuncnv  24015  ptcmpfi  24021  tsmsres  24352  imasdsf1olem  24581  tmslem  24690  tmsxms  24694  imasf1oxms  24697  prdsxms  24738  tmsxps  24744  tmsxpsmopn  24745  isngp2  24805  tngngp2  24860  cnfldms  24983  cncms  25565  cnfldcusp  25567  mbfres2  25855  dvres  26121  dvres3a  26124  cpnres  26147  dvmptres3  26166  dvlip2  26205  dvgt0lem2  26213  dvne0  26221  rlimcnp2  27182  jensen  27204  eupthvdres  30657  sspg  31151  ssps  31153  sspn  31159  hhsssh  31692  fnresin  33040  padct  33133  ffsrn  33143  resf1o  33145  indf1ofs  33256  symgcom  33467  cycpmconjvlem  33525  cycpmconjslem1  33538  nsgqusf1o  33789  ply1degltdimlem  34076  cnrrext  34464  eulerpartlemt  34826  subfacp1lem3  35711  subfacp1lem5  35713  cvmliftlem11  35824  poimirlem9  38337  dvun  43178  mapfzcons1  43506  eq0rabdioph  43565  eldioph4b  43596  diophren  43598  pwssplit4  43874  tfsconcatrev  44133  dvresntr  46690  sge0split  47181  imaidfu2  49946