Theorem fnresdm 5701

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 5690	. 2 |- ( F Fn A -> Rel F )
2		fndm 5691	. . 3 |- ( F Fn A -> dom F = A )
3		eqimss 3517	. . 3 |- ( dom F = A -> dom F C_ A )
4	2, 3	syl 17	. 2 |- ( F Fn A -> dom F C_ A )
5		relssres 5159	. 2 |- ( ( Rel F /\ dom F C_ A ) -> ( F |` A ) = F )
6	1, 4, 5	syl2anc 666	1 |- ( F Fn A -> ( F |` A ) = F )

Syntax hints:   -> wi 4   = wceq 1438   C_ wss 3437   dom cdm 4851   |` cres 4853   Rel wrel 4856   Fn wfn 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-xp 4857  df-rel 4858  df-dm 4861  df-res 4863  df-fun 5601  df-fn 5602

This theorem is referenced by:  fnima  5710  fresin  5767  resasplit  5768  fresaunres2  5770  fvreseq1  5996  fnsnb  6096  fninfp  6104  fnsnsplit  6114  fsnunfv  6117  fsnunres  6118  fnsuppeq0  6952  mapunen  7745  fnfi  7853  canthp1lem2  9080  fseq1p1m1  11870  facnn  12462  fac0  12463  hashgval  12519  hashinf  12521  rlimres  13615  lo1res  13616  rlimresb  13622  isercolllem2  13722  isercoll  13724  ruclem4  14279  fsets  15142  sscres  15721  sscid  15722  gsumzres  17536  pwssplit1  18275  zzngim  19115  ptuncnv  20814  ptcmpfi  20820  tsmsres  21150  imasdsf1olem  21380  tmslem  21489  tmsxms  21493  imasf1oxms  21496  prdsxms  21537  tmsxps  21543  tmsxpsmopn  21544  isngp2  21603  tngngp2  21652  cnfldms  21788  cncms  22314  cnfldcusp  22316  mbfres2  22593  dvres  22858  dvres3a  22861  cpnres  22883  dvmptres3  22902  dvlip2  22939  dvgt0lem2  22947  dvne0  22955  rlimcnp2  23884  jensen  23906  eupath2  25700  subgores  26024  sspg  26359  ssps  26361  sspn  26367  hhsssh  26912  fnresin  28224  padct  28307  ffsrn  28314  resf1o  28315  gsumle  28543  cnrrext  28816  indf1ofs  28849  eulerpartlemt  29206  bnj142OLD  29536  subfacp1lem3  29907  subfacp1lem5  29909  cvmliftlem11  30020  poimirlem9  31869  mapfzcons1  35484  eq0rabdioph  35544  eldioph4b  35579  diophren  35581  pwssplit4  35873  dvresntr  37614  sge0split  38045