Theorem fnresdm 6688

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900  dom cdm 5658   ↾ cres 5660  Rel wrel 5663   Fn wfn 6561

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-dm 5668  df-res 5670  df-fun 6568  df-fn 6569

This theorem is used by:  fnima  6699  fresin  6781  resasplit  6782  fresaunres2  6784  fvreseq1  7069  fnsnr  7200  fninfp  7210  fnsnsplit  7220  fsnunfv  7223  fsnunres  7224  fnsuppeq0  8247  mapunen  9203  dif1enlem  9213  fnfi  9231  canthp1lem2  10777  fseq1p1m1  13772  facnn  14460  fac0  14461  hashgval  14518  hashinf  14520  rlimres  15769  lo1res  15770  rlimresb  15776  isercolllem2  15877  isercoll  15879  ruclem4  16446  fsets  17391  sscres  18048  sscid  18049  gsumzres  20174  gsumle  20410  pwssplit1  21385  zzngim  21913  ptuncnv  24181  ptcmpfi  24187  tsmsres  24518  imasdsf1olem  24747  tmslem  24856  tmsxms  24860  imasf1oxms  24863  prdsxms  24904  tmsxps  24910  tmsxpsmopn  24911  isngp2  24971  tngngp2  25026  cnfldms  25149  cncms  25731  cnfldcusp  25733  mbfres2  26021  dvres  26286  dvres3a  26289  cpnres  26312  dvmptres3  26331  dvlip2  26370  dvgt0lem2  26378  dvne0  26386  rlimcnp2  27351  jensen  27373  eupthvdres  30893  sspg  31387  ssps  31389  sspn  31395  hhsssh  31928  fnresin  33316  padct  33407  ffsrn  33416  resf1o  33418  indf1ofs  33529  symgcom  33743  cycpmconjvlem  33801  cycpmconjslem1  33814  nsgqusf1o  34071  ply1degltdimlem  34365  cnrrext  34753  eulerpartlemt  35114  subfacp1lem3  36155  subfacp1lem5  36157  cvmliftlem11  36268  poimirlem9  38815  dvun  43676  mapfzcons1  43994  eq0rabdioph  44053  eldioph4b  44084  diophren  44086  pwssplit4  44357  tfsconcatrev  44611  dvresntr  47201  sge0split  47692  imaidfu2  50558