Theorem fnresdm 6246

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 6234	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6235	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3876	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 5687	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 579	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1601   ⊆ wss 3792  dom cdm 5355   ↾ cres 5357  Rel wrel 5360   Fn wfn 6130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-xp 5361  df-rel 5362  df-dm 5365  df-res 5367  df-fun 6137  df-fn 6138

This theorem is referenced by:  fnima  6256  fresin  6323  resasplit  6324  fresaunres2  6326  fvreseq1  6581  fnsnr  6698  fninfp  6707  fnsnsplit  6721  fsnunfv  6724  fsnunres  6725  fnsuppeq0  7605  mapunen  8417  fnfi  8526  canthp1lem2  9810  fseq1p1m1  12732  facnn  13380  fac0  13381  hashgval  13438  hashinf  13440  rlimres  14697  lo1res  14698  rlimresb  14704  isercolllem2  14804  isercoll  14806  ruclem4  15367  fsets  16288  sscres  16868  sscid  16869  gsumzres  18696  pwssplit1  19454  zzngim  20296  ptuncnv  22019  ptcmpfi  22025  tsmsres  22355  imasdsf1olem  22586  tmslem  22695  tmsxms  22699  imasf1oxms  22702  prdsxms  22743  tmsxps  22749  tmsxpsmopn  22750  isngp2  22809  tngngp2  22864  cnfldms  22987  cncms  23561  cnfldcusp  23563  mbfres2  23849  dvres  24112  dvres3a  24115  cpnres  24137  dvmptres3  24156  dvlip2  24195  dvgt0lem2  24203  dvne0  24211  rlimcnp2  25145  jensen  25167  eupthvdres  27639  sspg  28155  ssps  28157  sspn  28163  hhsssh  28698  fnresin  29995  padct  30063  ffsrn  30070  resf1o  30071  gsumle  30341  cnrrext  30652  indf1ofs  30686  eulerpartlemt  31031  subfacp1lem3  31763  subfacp1lem5  31765  cvmliftlem11  31876  poimirlem9  34046  mapfzcons1  38244  eq0rabdioph  38304  eldioph4b  38339  diophren  38341  pwssplit4  38622  dvresntr  41064  sge0split  41554