Theorem fnresdm 5681

Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)

Assertion

Ref	Expression
fnresdm	|- ( F Fn A -> ( F |` A ) = F )

Proof of Theorem fnresdm

Step	Hyp	Ref	Expression
1		fnrel 5670	. 2 |- ( F Fn A -> Rel F )
2		fndm 5671	. . 3 |- ( F Fn A -> dom F = A )
3		eqimss 3549	. . 3 |- ( dom F = A -> dom F C_ A )
4	2, 3	syl 16	. 2 |- ( F Fn A -> dom F C_ A )
5		relssres 5302	. 2 |- ( ( Rel F /\ dom F C_ A ) -> ( F |` A ) = F )
6	1, 4, 5	syl2anc 661	1 |- ( F Fn A -> ( F |` A ) = F )

Syntax hints:   -> wi 4   = wceq 1374   C_ wss 3469   dom cdm 4992   |` cres 4994   Rel wrel 4997   Fn wfn 5574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-xp 4998  df-rel 4999  df-dm 5002  df-res 5004  df-fun 5581  df-fn 5582

This theorem is referenced by:  fnima  5690  fresin  5745  resasplit  5746  fresaunres2  5748  fvreseq1  5973  fnsnb  6071  fninfp  6079  fnsnsplit  6089  fsnunfv  6092  fsnunres  6093  fnsuppeq0OLD  6113  fnsuppeq0  6918  mapunen  7676  fnfi  7787  canthp1lem2  9020  fseq1p1m1  11741  facnn  12310  fac0  12311  hashgval  12363  hashinf  12365  rlimres  13330  lo1res  13331  rlimresb  13337  isercolllem2  13437  isercoll  13439  ruclem4  13817  fsets  14505  sscres  15042  sscid  15043  gsumzres  16698  gsumzresOLD  16702  pwssplit1  17481  zzngim  18351  ptuncnv  20036  ptcmpfi  20042  tsmsresOLD  20373  tsmsres  20374  imasdsf1olem  20604  tmslem  20713  tmsxms  20717  imasf1oxms  20720  prdsxms  20761  tmsxps  20767  tmsxpsmopn  20768  isngp2  20845  tngngp2  20894  cnfldms  21011  cncms  21523  cnfldcusp  21525  mbfres2  21780  dvres  22043  dvres3a  22046  cpnres  22068  dvmptres3  22087  dvlip2  22124  dvgt0lem2  22132  dvne0  22140  rlimcnp2  23017  jensen  23039  eupath2  24642  subgores  24968  sspg  25303  ssps  25305  sspn  25311  hhsssh  25847  fnresin  27129  ffsrn  27210  resf1o  27211  gsumle  27419  cnrrext  27613  indf1ofs  27665  eulerpartlemt  27936  subfacp1lem3  28252  subfacp1lem5  28254  cvmliftlem11  28366  mapfzcons1  30240  eq0rabdioph  30301  eldioph4b  30336  diophren  30338  pwssplit4  30628  icccncfext  31181  dvresntr  31201  bnj142OLD  32736