MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnresdm Unicode version

Theorem fnresdm 5695
Description: A function does not change when restricted to its domain. (Contributed by NM, 5-Sep-2004.)
Assertion
Ref Expression
fnresdm

Proof of Theorem fnresdm
StepHypRef Expression
1 fnrel 5684 . 2
2 fndm 5685 . . 3
3 eqimss 3555 . . 3
42, 3syl 16 . 2
5 relssres 5316 . 2
61, 4, 5syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475  domcdm 5004  |`cres 5006  Relwrel 5009  Fnwfn 5588
This theorem is referenced by:  fnima  5704  fresin  5759  resasplit  5760  fresaunres2  5762  fvreseq1  5988  fnsnb  6090  fninfp  6098  fnsnsplit  6108  fsnunfv  6111  fsnunres  6112  fnsuppeq0OLD  6132  fnsuppeq0  6947  mapunen  7706  fnfi  7818  canthp1lem2  9052  fseq1p1m1  11781  facnn  12355  fac0  12356  hashgval  12408  hashinf  12410  rlimres  13381  lo1res  13382  rlimresb  13388  isercolllem2  13488  isercoll  13490  ruclem4  13967  fsets  14658  sscres  15192  sscid  15193  gsumzres  16914  gsumzresOLD  16918  pwssplit1  17705  zzngim  18591  ptuncnv  20308  ptcmpfi  20314  tsmsresOLD  20645  tsmsres  20646  imasdsf1olem  20876  tmslem  20985  tmsxms  20989  imasf1oxms  20992  prdsxms  21033  tmsxps  21039  tmsxpsmopn  21040  isngp2  21117  tngngp2  21166  cnfldms  21283  cncms  21795  cnfldcusp  21797  mbfres2  22052  dvres  22315  dvres3a  22318  cpnres  22340  dvmptres3  22359  dvlip2  22396  dvgt0lem2  22404  dvne0  22412  rlimcnp2  23296  jensen  23318  eupath2  24980  subgores  25306  sspg  25641  ssps  25643  sspn  25649  hhsssh  26185  fnresin  27470  ffsrn  27552  resf1o  27553  gsumle  27770  cnrrext  27991  indf1ofs  28039  eulerpartlemt  28310  subfacp1lem3  28626  subfacp1lem5  28628  cvmliftlem11  28740  mapfzcons1  30649  eq0rabdioph  30710  eldioph4b  30745  diophren  30747  pwssplit4  31035  dvresntr  31713  bnj142OLD  33781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-dm 5014  df-res 5016  df-fun 5595  df-fn 5596
  Copyright terms: Public domain W3C validator