Theorem fnresdm 6619

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 6602	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6603	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3994	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5989	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 585	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903  dom cdm 5632   ↾ cres 5634  Rel wrel 5637   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-dm 5642  df-res 5644  df-fun 6502  df-fn 6503

This theorem is referenced by:  fnima  6630  fresin  6711  resasplit  6712  fresaunres2  6714  fvreseq1  6993  fnsnr  7119  fninfp  7130  fnsnsplit  7140  fsnunfv  7143  fsnunres  7144  fnsuppeq0  8144  mapunen  9086  dif1enlem  9096  fnfi  9114  canthp1lem2  10576  fseq1p1m1  13526  facnn  14210  fac0  14211  hashgval  14268  hashinf  14270  rlimres  15493  lo1res  15494  rlimresb  15500  isercolllem2  15601  isercoll  15603  ruclem4  16171  fsets  17108  sscres  17759  sscid  17760  gsumzres  19850  gsumle  20086  pwssplit1  21023  zzngim  21519  ptuncnv  23763  ptcmpfi  23769  tsmsres  24100  imasdsf1olem  24329  tmslem  24438  tmsxms  24442  imasf1oxms  24445  prdsxms  24486  tmsxps  24492  tmsxpsmopn  24493  isngp2  24553  tngngp2  24608  cnfldms  24731  cncms  25323  cnfldcusp  25325  mbfres2  25614  dvres  25880  dvres3a  25883  cpnres  25907  dvmptres3  25928  dvlip2  25968  dvgt0lem2  25976  dvne0  25984  rlimcnp2  26944  jensen  26967  eupthvdres  30322  sspg  30816  ssps  30818  sspn  30824  hhsssh  31357  fnresin  32714  padct  32808  ffsrn  32818  resf1o  32820  indf1ofs  32959  symgcom  33177  cycpmconjvlem  33235  cycpmconjslem1  33248  nsgqusf1o  33509  ply1degltdimlem  33800  cnrrext  34188  eulerpartlemt  34549  subfacp1lem3  35398  subfacp1lem5  35400  cvmliftlem11  35511  poimirlem9  37880  dvun  42729  mapfzcons1  43074  eq0rabdioph  43133  eldioph4b  43168  diophren  43170  pwssplit4  43446  tfsconcatrev  43705  dvresntr  46276  sge0split  46767  imaidfu2  49470