Theorem fnresdm 5520

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 5509	. 2 |- ( F Fn A -> Rel F )
2		fndm 5510	. . 3 |- ( F Fn A -> dom F = A )
3		eqimss 3408	. . 3 |- ( dom F = A -> dom F C_ A )
4	2, 3	syl 16	. 2 |- ( F Fn A -> dom F C_ A )
5		relssres 5147	. 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 1369   C_ wss 3328   dom cdm 4840   |` cres 4842   Rel wrel 4845   Fn wfn 5413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-xp 4846  df-rel 4847  df-dm 4850  df-res 4852  df-fun 5420  df-fn 5421

This theorem is referenced by:  fnima  5529  fresin  5580  resasplit  5581  fresaunres2  5583  fvreseq1  5804  fnsnb  5898  fninfp  5905  fnsnsplit  5915  fsnunfv  5918  fsnunres  5919  fnsuppeq0OLD  5939  fnsuppeq0  6717  mapunen  7480  fnfi  7589  canthp1lem2  8820  fseq1p1m1  11534  facnn  12053  fac0  12054  hashgval  12106  hashinf  12108  rlimres  13036  lo1res  13037  rlimresb  13043  isercolllem2  13143  isercoll  13145  ruclem4  13516  fsets  14200  sscres  14736  sscid  14737  gsumzres  16388  gsumzresOLD  16392  pwssplit1  17140  zzngim  17985  ptuncnv  19380  ptcmpfi  19386  tsmsresOLD  19717  tsmsres  19718  imasdsf1olem  19948  tmslem  20057  tmsxms  20061  imasf1oxms  20064  prdsxms  20105  tmsxps  20111  tmsxpsmopn  20112  isngp2  20189  tngngp2  20238  cnfldms  20355  cncms  20867  cnfldcusp  20869  mbfres2  21123  dvres  21386  dvres3a  21389  cpnres  21411  dvmptres3  21430  dvlip2  21467  dvgt0lem2  21475  dvne0  21483  rlimcnp2  22360  jensen  22382  eupath2  23601  subgores  23791  sspg  24126  ssps  24128  sspn  24134  hhsssh  24670  fnresin  25947  ffsrn  26029  resf1o  26030  gsumle  26246  cnrrext  26439  indf1ofs  26482  eulerpartlemt  26754  subfacp1lem3  27070  subfacp1lem5  27072  cvmliftlem11  27184  mapfzcons1  29053  eq0rabdioph  29115  eldioph4b  29150  diophren  29152  pwssplit4  29442  bnj142OLD  31717