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

Theorem reseq2i 5085
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 5083 . 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 1649    |` cres 4822
This theorem is referenced by:  reseq12i  5086  rescom  5113  rescnvcnv  5274  resdm2  5302  funcnvres  5464  resasplit  5555  fresaunres2  5557  fresaunres1  5558  resdif  5638  resin  5639  domss2  7204  ordtypelem1  7422  ackbij2lem3  8056  facnn  11497  fac0  11498  ruclem4  12762  setsid  13437  dprd2da  15529  ply1plusgfvi  16565  uptx  17580  txcn  17581  ressxms  18447  ressms  18448  iscmet3lem3  19116  volres  19293  dvlip  19746  dvne0  19764  lhop  19769  dflog2  20327  dfrelog  20332  dvlog  20411  wilthlem2  20721  0pth  21426  2pthonlem1  21449  ghsubgolem  21808  zrdivrng  21870  df1stres  23934  df2ndres  23935  hashresfn  23996  divcnvshft  24992  divcnvlin  24993  wfrlem5  25286  frrlem5  25311  isdrngo1  26265  eldioph4b  26565  diophren  26567  seff  27209  sblpnf  27210  bnj1326  28735
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-in 3272  df-opab 4210  df-xp 4826  df-res 4832
  Copyright terms: Public domain W3C validator