Theorem fnresdm 6640

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917  dom cdm 5641   ↾ cres 5643  Rel wrel 5646   Fn wfn 6509

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-dm 5651  df-res 5653  df-fun 6516  df-fn 6517

This theorem is referenced by:  fnima  6651  fresin  6732  resasplit  6733  fresaunres2  6735  fvreseq1  7014  fnsnr  7140  fninfp  7151  fnsnsplit  7161  fsnunfv  7164  fsnunres  7165  fnsuppeq0  8174  mapunen  9116  dif1enlem  9126  dif1enlemOLD  9127  fnfi  9148  canthp1lem2  10613  fseq1p1m1  13566  facnn  14247  fac0  14248  hashgval  14305  hashinf  14307  rlimres  15531  lo1res  15532  rlimresb  15538  isercolllem2  15639  isercoll  15641  ruclem4  16209  fsets  17146  sscres  17792  sscid  17793  gsumzres  19846  pwssplit1  20973  zzngim  21469  ptuncnv  23701  ptcmpfi  23707  tsmsres  24038  imasdsf1olem  24268  tmslem  24377  tmsxms  24381  imasf1oxms  24384  prdsxms  24425  tmsxps  24431  tmsxpsmopn  24432  isngp2  24492  tngngp2  24547  cnfldms  24670  cncms  25262  cnfldcusp  25264  mbfres2  25553  dvres  25819  dvres3a  25822  cpnres  25846  dvmptres3  25867  dvlip2  25907  dvgt0lem2  25915  dvne0  25923  rlimcnp2  26883  jensen  26906  eupthvdres  30171  sspg  30664  ssps  30666  sspn  30672  hhsssh  31205  fnresin  32557  padct  32650  ffsrn  32659  resf1o  32660  indf1ofs  32796  gsumle  33045  symgcom  33047  cycpmconjvlem  33105  cycpmconjslem1  33118  nsgqusf1o  33394  ply1degltdimlem  33625  cnrrext  34007  eulerpartlemt  34369  subfacp1lem3  35176  subfacp1lem5  35178  cvmliftlem11  35289  poimirlem9  37630  dvun  42354  mapfzcons1  42712  eq0rabdioph  42771  eldioph4b  42806  diophren  42808  pwssplit4  43085  tfsconcatrev  43344  dvresntr  45923  sge0split  46414  imaidfu2  49104