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

Theorem reseq2i 4952
Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqi.1  |-  A  =  B
Assertion
Ref Expression
reseq2i  |-  ( C  |`  A )  =  ( C  |`  B )

Proof of Theorem reseq2i
StepHypRef Expression
1 reseqi.1 . 2  |-  A  =  B
2 reseq2 4950 . 2  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
31, 2ax-mp 8 1  |-  ( C  |`  A )  =  ( C  |`  B )
Colors of variables: wff set class
Syntax hints:    = wceq 1623    |` cres 4691
This theorem is referenced by:  reseq12i  4953  rescom  4980  rescnvcnv  5135  resdm2  5163  funcnvres  5321  resasplit  5411  fresaunres2  5413  fresaunres1  5414  resdif  5494  resin  5495  domss2  7020  ordtypelem1  7233  ackbij2lem3  7867  facnn  11290  fac0  11291  ruclem4  12512  setsid  13187  dprd2da  15277  ply1plusgfvi  16320  uptx  17319  txcn  17320  ressxms  18071  ressms  18072  iscmet3lem3  18716  volres  18887  dvlip  19340  dvne0  19358  lhop  19363  dflog2  19918  dfrelog  19923  dvlog  19998  wilthlem2  20307  ghsubgolem  21037  zrdivrng  21099  hashresfn  23173  df1stres  23243  df2ndres  23244  wfrlem5  24260  frrlem5  24285  domrancur1c  25202  empos  25242  dispos  25287  isdrngo1  26587  eldioph4b  26894  diophren  26896  seff  27538  sblpnf  27539  bnj1326  29056
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-opab 4078  df-xp 4695  df-res 4701
  Copyright terms: Public domain W3C validator