Theorem fnresdm 6663

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 6646	. 2 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		fndm 6647	. . 3 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3		eqimss 3967	. . 3 ⊢ (dom 𝐹 = 𝐴 → dom 𝐹 ⊆ 𝐴)
4	2, 3	syl 18	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 ⊆ 𝐴)
5		relssres 6013	. 2 ⊢ ((Rel 𝐹 ∧ dom 𝐹 ⊆ 𝐴) → (𝐹 ↾ 𝐴) = 𝐹)
6	1, 4, 5	syl2anc 596	1 ⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3896  dom cdm 5651   ↾ cres 5653  Rel wrel 5656   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5657  df-rel 5658  df-dm 5661  df-res 5663  df-fun 6545  df-fn 6546

This theorem is used by:  fnima  6674  fresin  6756  resasplit  6757  fresaunres2  6759  fvreseq1  7043  fnsnr  7173  fninfp  7183  fnsnsplit  7193  fsnunfv  7196  fsnunres  7197  fnsuppeq0  8216  mapunen  9172  dif1enlem  9182  fnfi  9200  canthp1lem2  10745  fseq1p1m1  13739  facnn  14426  fac0  14427  hashgval  14484  hashinf  14486  rlimres  15734  lo1res  15735  rlimresb  15741  isercolllem2  15842  isercoll  15844  ruclem4  16411  fsets  17356  sscres  18007  sscid  18008  gsumzres  20132  gsumle  20368  pwssplit1  21343  zzngim  21867  ptuncnv  24135  ptcmpfi  24141  tsmsres  24472  imasdsf1olem  24701  tmslem  24810  tmsxms  24814  imasf1oxms  24817  prdsxms  24858  tmsxps  24864  tmsxpsmopn  24865  isngp2  24925  tngngp2  24980  cnfldms  25103  cncms  25685  cnfldcusp  25687  mbfres2  25975  dvres  26240  dvres3a  26243  cpnres  26266  dvmptres3  26285  dvlip2  26324  dvgt0lem2  26332  dvne0  26340  rlimcnp2  27303  jensen  27325  eupthvdres  30845  sspg  31339  ssps  31341  sspn  31347  hhsssh  31880  fnresin  33269  padct  33361  ffsrn  33370  resf1o  33372  indf1ofs  33483  symgcom  33694  cycpmconjvlem  33752  cycpmconjslem1  33765  nsgqusf1o  34017  ply1degltdimlem  34304  cnrrext  34692  eulerpartlemt  35053  subfacp1lem3  36037  subfacp1lem5  36039  cvmliftlem11  36150  poimirlem9  38656  dvun  43519  mapfzcons1  43837  eq0rabdioph  43896  eldioph4b  43927  diophren  43929  pwssplit4  44200  tfsconcatrev  44459  dvresntr  47036  sge0split  47527  imaidfu2  50335