Theorem fnresdm 6000

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 5989	. 2 |- ( F Fn A -> Rel F )
2		fndm 5990	. . 3 |- ( F Fn A -> dom F = A )
3		eqimss 3657	. . 3 |- ( dom F = A -> dom F C_ A )
4	2, 3	syl 17	. 2 |- ( F Fn A -> dom F C_ A )
5		relssres 5437	. 2 |- ( ( Rel F /\ dom F C_ A ) -> ( F |` A ) = F )
6	1, 4, 5	syl2anc 693	1 |- ( F Fn A -> ( F |` A ) = F )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574   dom cdm 5114   |` cres 5116   Rel wrel 5119   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-dm 5124  df-res 5126  df-fun 5890  df-fn 5891

This theorem is referenced by:  fnima  6010  fresin  6073  resasplit  6074  fresaunres2  6076  fvreseq1  6318  fnsnb  6432  fninfp  6440  fnsnsplit  6450  fsnunfv  6453  fsnunres  6454  fnsuppeq0  7323  mapunen  8129  fnfi  8238  canthp1lem2  9475  fseq1p1m1  12414  facnn  13062  fac0  13063  hashgval  13120  hashinf  13122  rlimres  14289  lo1res  14290  rlimresb  14296  isercolllem2  14396  isercoll  14398  ruclem4  14963  fsets  15891  sscres  16483  sscid  16484  gsumzres  18310  pwssplit1  19059  zzngim  19901  ptuncnv  21610  ptcmpfi  21616  tsmsres  21947  imasdsf1olem  22178  tmslem  22287  tmsxms  22291  imasf1oxms  22294  prdsxms  22335  tmsxps  22341  tmsxpsmopn  22342  isngp2  22401  tngngp2  22456  cnfldms  22579  cncms  23151  cnfldcusp  23153  mbfres2  23412  dvres  23675  dvres3a  23678  cpnres  23700  dvmptres3  23719  dvlip2  23758  dvgt0lem2  23766  dvne0  23774  rlimcnp2  24693  jensen  24715  eupthvdres  27095  sspg  27583  ssps  27585  sspn  27591  hhsssh  28126  fnresin  29430  padct  29497  ffsrn  29504  resf1o  29505  gsumle  29779  cnrrext  30054  indf1ofs  30088  eulerpartlemt  30433  bnj142OLD  30794  subfacp1lem3  31164  subfacp1lem5  31166  cvmliftlem11  31277  poimirlem9  33418  mapfzcons1  37280  eq0rabdioph  37340  eldioph4b  37375  diophren  37377  pwssplit4  37659  dvresntr  40132  sge0split  40626