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

Theorem reseq2i 5135
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 5133 . 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 1652    |` cres 4872
This theorem is referenced by:  reseq12i  5136  rescom  5163  rescnvcnv  5324  resdm2  5352  funcnvres  5514  resasplit  5605  fresaunres2  5607  fresaunres1  5608  resdif  5688  resin  5689  domss2  7258  ordtypelem1  7479  ackbij2lem3  8113  facnn  11560  fac0  11561  ruclem4  12825  setsid  13500  dprd2da  15592  ply1plusgfvi  16628  uptx  17649  txcn  17650  ressxms  18547  ressms  18548  iscmet3lem3  19235  volres  19416  dvlip  19869  dvne0  19887  lhop  19892  dflog2  20450  dfrelog  20455  dvlog  20534  wilthlem2  20844  0pth  21562  2pthlem1  21587  ghsubgolem  21950  zrdivrng  22012  df1stres  24083  df2ndres  24084  hashresfn  24148  sitmcl  24655  divcnvshft  25203  divcnvlin  25204  wfrlem5  25534  frrlem5  25578  isdrngo1  26563  eldioph4b  26863  diophren  26865  seff  27506  sblpnf  27507  bnj1326  29332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-in 3319  df-opab 4259  df-xp 4876  df-res 4882
  Copyright terms: Public domain W3C validator