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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3911  dom cdm 5631   ↾ cres 5633  Rel wrel 5636   Fn wfn 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638  df-dm 5641  df-res 5643  df-fun 6501  df-fn 6502

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  8148  mapunen  9087  dif1enlem  9097  dif1enlemOLD  9098  fnfi  9119  canthp1lem2  10582  fseq1p1m1  13535  facnn  14216  fac0  14217  hashgval  14274  hashinf  14276  rlimres  15500  lo1res  15501  rlimresb  15507  isercolllem2  15608  isercoll  15610  ruclem4  16178  fsets  17115  sscres  17761  sscid  17762  gsumzres  19815  pwssplit1  20942  zzngim  21438  ptuncnv  23670  ptcmpfi  23676  tsmsres  24007  imasdsf1olem  24237  tmslem  24346  tmsxms  24350  imasf1oxms  24353  prdsxms  24394  tmsxps  24400  tmsxpsmopn  24401  isngp2  24461  tngngp2  24516  cnfldms  24639  cncms  25231  cnfldcusp  25233  mbfres2  25522  dvres  25788  dvres3a  25791  cpnres  25815  dvmptres3  25836  dvlip2  25876  dvgt0lem2  25884  dvne0  25892  rlimcnp2  26852  jensen  26875  eupthvdres  30137  sspg  30630  ssps  30632  sspn  30638  hhsssh  31171  fnresin  32523  padct  32616  ffsrn  32625  resf1o  32626  indf1ofs  32762  gsumle  33011  symgcom  33013  cycpmconjvlem  33071  cycpmconjslem1  33084  nsgqusf1o  33360  ply1degltdimlem  33591  cnrrext  33973  eulerpartlemt  34335  subfacp1lem3  35142  subfacp1lem5  35144  cvmliftlem11  35255  poimirlem9  37596  dvun  42320  mapfzcons1  42678  eq0rabdioph  42737  eldioph4b  42772  diophren  42774  pwssplit4  43051  tfsconcatrev  43310  dvresntr  45889  sge0split  46380  imaidfu2  49073