Theorem fnresdm 6535

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 6519	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6520	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3973	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5921	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 583	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883  dom cdm 5580   ↾ cres 5582  Rel wrel 5585   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-dm 5590  df-res 5592  df-fun 6420  df-fn 6421

This theorem is referenced by:  fnima  6547  fresin  6627  resasplit  6628  fresaunres2  6630  fvreseq1  6898  fnsnr  7019  fninfp  7028  fnsnsplit  7038  fsnunfv  7041  fsnunres  7042  fnsuppeq0  7979  mapunen  8882  dif1enlem  8905  fnfi  8925  canthp1lem2  10340  fseq1p1m1  13259  facnn  13917  fac0  13918  hashgval  13975  hashinf  13977  rlimres  15195  lo1res  15196  rlimresb  15202  isercolllem2  15305  isercoll  15307  ruclem4  15871  fsets  16798  sscres  17452  sscid  17453  gsumzres  19425  rnrhmsubrg  19971  pwssplit1  20236  zzngim  20672  ptuncnv  22866  ptcmpfi  22872  tsmsres  23203  imasdsf1olem  23434  tmslem  23543  tmslemOLD  23544  tmsxms  23548  imasf1oxms  23551  prdsxms  23592  tmsxps  23598  tmsxpsmopn  23599  isngp2  23659  tngngp2  23722  cnfldms  23845  cncms  24424  cnfldcusp  24426  mbfres2  24714  dvres  24980  dvres3a  24983  cpnres  25006  dvmptres3  25025  dvlip2  25064  dvgt0lem2  25072  dvne0  25080  rlimcnp2  26021  jensen  26043  eupthvdres  28500  sspg  28991  ssps  28993  sspn  28999  hhsssh  29532  fnresin  30862  padct  30956  ffsrn  30966  resf1o  30967  gsumle  31252  symgcom  31254  cycpmconjvlem  31310  cycpmconjslem1  31323  nsgqusf1o  31503  cnrrext  31860  indf1ofs  31894  eulerpartlemt  32238  subfacp1lem3  33044  subfacp1lem5  33046  cvmliftlem11  33157  poimirlem9  35713  mapfzcons1  40455  eq0rabdioph  40514  eldioph4b  40549  diophren  40551  pwssplit4  40830  dvresntr  43349  sge0split  43837