Theorem fnresdm 5706

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 5695	. 2 |- ( F Fn A -> Rel F )
2		fndm 5696	. . 3 |- ( F Fn A -> dom F = A )
3		eqimss 3495	. . 3 |- ( dom F = A -> dom F C_ A )
4	2, 3	syl 17	. 2 |- ( F Fn A -> dom F C_ A )
5		relssres 5160	. 2 |- ( ( Rel F /\ dom F C_ A ) -> ( F |` A ) = F )
6	1, 4, 5	syl2anc 671	1 |- ( F Fn A -> ( F |` A ) = F )

Syntax hints:   -> wi 4   = wceq 1454   C_ wss 3415   dom cdm 4852   |` cres 4854   Rel wrel 4857   Fn wfn 5595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-xp 4858  df-rel 4859  df-dm 4862  df-res 4864  df-fun 5602  df-fn 5603

This theorem is referenced by:  fnima  5715  fresin  5774  resasplit  5775  fresaunres2  5777  fvreseq1  6005  fnsnb  6106  fninfp  6114  fnsnsplit  6124  fsnunfv  6127  fsnunres  6128  fnsuppeq0  6969  mapunen  7766  fnfi  7874  canthp1lem2  9103  fseq1p1m1  11896  facnn  12492  fac0  12493  hashgval  12549  hashinf  12551  rlimres  13670  lo1res  13671  rlimresb  13677  isercolllem2  13777  isercoll  13779  ruclem4  14334  fsets  15197  sscres  15776  sscid  15777  gsumzres  17591  pwssplit1  18330  zzngim  19171  ptuncnv  20870  ptcmpfi  20876  tsmsres  21206  imasdsf1olem  21436  tmslem  21545  tmsxms  21549  imasf1oxms  21552  prdsxms  21593  tmsxps  21599  tmsxpsmopn  21600  isngp2  21659  tngngp2  21708  cnfldms  21844  cncms  22370  cnfldcusp  22372  mbfres2  22649  dvres  22914  dvres3a  22917  cpnres  22939  dvmptres3  22958  dvlip2  22995  dvgt0lem2  23003  dvne0  23011  rlimcnp2  23940  jensen  23962  eupath2  25756  subgores  26080  sspg  26415  ssps  26417  sspn  26423  hhsssh  26968  fnresin  28276  padct  28355  ffsrn  28362  resf1o  28363  gsumle  28590  cnrrext  28862  indf1ofs  28895  eulerpartlemt  29252  bnj142OLD  29582  subfacp1lem3  29953  subfacp1lem5  29955  cvmliftlem11  30066  poimirlem9  31993  mapfzcons1  35603  eq0rabdioph  35663  eldioph4b  35698  diophren  35700  pwssplit4  35991  dvresntr  37825  sge0split  38288