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 4054	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6042	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 584	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963  dom cdm 5689   ↾ cres 5691  Rel wrel 5694   Fn wfn 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-dm 5699  df-res 5701  df-fun 6565  df-fn 6566

This theorem is referenced by:  fnima  6699  fresin  6778  resasplit  6779  fresaunres2  6781  fvreseq1  7059  fnsnr  7185  fninfp  7194  fnsnsplit  7204  fsnunfv  7207  fsnunres  7208  fnsuppeq0  8216  mapunen  9185  dif1enlem  9195  dif1enlemOLD  9196  fnfi  9216  canthp1lem2  10691  fseq1p1m1  13635  facnn  14311  fac0  14312  hashgval  14369  hashinf  14371  rlimres  15591  lo1res  15592  rlimresb  15598  isercolllem2  15699  isercoll  15701  ruclem4  16267  fsets  17203  sscres  17871  sscid  17872  gsumzres  19942  pwssplit1  21076  zzngim  21589  ptuncnv  23831  ptcmpfi  23837  tsmsres  24168  imasdsf1olem  24399  tmslem  24510  tmslemOLD  24511  tmsxms  24515  imasf1oxms  24518  prdsxms  24559  tmsxps  24565  tmsxpsmopn  24566  isngp2  24626  tngngp2  24689  cnfldms  24812  cncms  25403  cnfldcusp  25405  mbfres2  25694  dvres  25961  dvres3a  25964  cpnres  25988  dvmptres3  26009  dvlip2  26049  dvgt0lem2  26057  dvne0  26065  rlimcnp2  27024  jensen  27047  eupthvdres  30264  sspg  30757  ssps  30759  sspn  30765  hhsssh  31298  fnresin  32643  padct  32737  ffsrn  32747  resf1o  32748  gsumle  33084  symgcom  33086  cycpmconjvlem  33144  cycpmconjslem1  33157  nsgqusf1o  33424  ply1degltdimlem  33650  cnrrext  33973  indf1ofs  34007  eulerpartlemt  34353  subfacp1lem3  35167  subfacp1lem5  35169  cvmliftlem11  35280  poimirlem9  37616  dvun  42368  mapfzcons1  42705  eq0rabdioph  42764  eldioph4b  42799  diophren  42801  pwssplit4  43078  tfsconcatrev  43338  dvresntr  45874  sge0split  46365