Theorem fnresdm 6656

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 6639	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6640	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3989	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 18	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6011	. 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 5651   ↾ cres 5653  Rel wrel 5656   Fn wfn 6532

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-rel 5658  df-dm 5661  df-res 5663  df-fun 6539  df-fn 6540

This theorem is used by:  fnima  6667  fresin  6749  resasplit  6750  fresaunres2  6752  fvreseq1  7036  fnsnr  7166  fninfp  7177  fnsnsplit  7187  fsnunfv  7190  fsnunres  7191  fnsuppeq0  8202  mapunen  9158  dif1enlem  9168  fnfi  9186  canthp1lem2  10731  fseq1p1m1  13725  facnn  14412  fac0  14413  hashgval  14470  hashinf  14472  rlimres  15718  lo1res  15719  rlimresb  15725  isercolllem2  15826  isercoll  15828  ruclem4  16395  fsets  17340  sscres  17991  sscid  17992  gsumzres  20116  gsumle  20352  pwssplit1  21327  zzngim  21851  ptuncnv  24119  ptcmpfi  24125  tsmsres  24456  imasdsf1olem  24685  tmslem  24794  tmsxms  24798  imasf1oxms  24801  prdsxms  24842  tmsxps  24848  tmsxpsmopn  24849  isngp2  24909  tngngp2  24964  cnfldms  25087  cncms  25669  cnfldcusp  25671  mbfres2  25959  dvres  26224  dvres3a  26227  cpnres  26250  dvmptres3  26269  dvlip2  26308  dvgt0lem2  26316  dvne0  26324  rlimcnp2  27287  jensen  27309  eupthvdres  30829  sspg  31323  ssps  31325  sspn  31331  hhsssh  31864  fnresin  33211  padct  33303  ffsrn  33313  resf1o  33315  indf1ofs  33426  symgcom  33637  cycpmconjvlem  33695  cycpmconjslem1  33708  nsgqusf1o  33960  ply1degltdimlem  34247  cnrrext  34635  eulerpartlemt  34996  subfacp1lem3  35926  subfacp1lem5  35928  cvmliftlem11  36039  poimirlem9  38527  dvun  43390  mapfzcons1  43707  eq0rabdioph  43766  eldioph4b  43797  diophren  43799  pwssplit4  44075  tfsconcatrev  44334  dvresntr  46897  sge0split  47388  imaidfu2  50188