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

Theorem reseq2d 4971
Description: Equality deduction for restrictions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
reseqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
reseq2d  |-  ( ph  ->  ( C  |`  A )  =  ( C  |`  B ) )

Proof of Theorem reseq2d
StepHypRef Expression
1 reseqd.1 . 2  |-  ( ph  ->  A  =  B )
2 reseq2 4966 . 2  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    |` cres 4707
This theorem is referenced by:  reseq12d  4972  resima2  5004  relresfld  5215  f1orescnv  5504  funcocnv2  5514  fococnv2  5515  fnressn  5721  fnsnsplit  5733  oprssov  6005  curry1  6226  curry2  6229  dftpos2  6267  tfrlem16  6425  sbthlem4  6990  mapunen  7046  hartogslem1  7273  axdc3lem2  8093  fseq1p1m1  10873  hashf1lem1  11409  setsval  13188  idfuval  13766  idfu2nd  13767  resf1st  13784  setcid  13934  catcisolem  13954  1stfval  13981  1stf2  13983  2ndfval  13984  2ndf2  13986  1stfcl  13987  2ndfcl  13988  curf2ndf  14037  hofcl  14049  isps  14327  cnvps  14337  isdir  14370  dirref  14373  tsrdir  14376  frmdval  14489  frmdplusg  14492  gsum2d  15239  dprd2da  15293  dpjval  15307  ablfac1eulem  15323  ablfac1eu  15324  psrplusg  16142  opsrtoslem2  16242  imacmp  17140  ptuncnv  17514  tgphaus  17815  tsmsres  17842  tsmsxplem1  17851  tsmsxplem2  17852  metreslem  17942  imasdsf1olem  17953  xmspropd  18035  mspropd  18036  imasf1oxms  18051  imasf1oms  18052  nmpropd2  18133  isngp2  18135  ngppropd  18169  tngngp2  18184  cmspropd  18787  mbfres2  19016  limciun  19260  dvmptres3  19321  dvmptres2  19327  dvmptntr  19336  dvlipcn  19357  dvlip2  19358  c1liplem1  19359  dvgt0lem1  19365  lhop1lem  19376  dvcnvrelem1  19380  dvcvx  19383  ftc2ditglem  19408  wilthlem2  20323  dchrval  20489  dchrelbas2  20492  efghgrp  21056  drngoi  21090  isdivrngo  21114  hhssablo  21856  hhssnvt  21858  hhsssh  21862  esumcvg  23469  itgmcntTMP  23603  cvmliftlem5  23835  cvmliftlem7  23837  cvmliftlem10  23840  cvmliftlem11  23841  cvmliftlem15  23844  cvmlift2lem11  23859  cvmlift2lem12  23860  eupath2lem3  23918  eupath2  23919  ghomgrplem  24011  relexp0  24040  relexpsucr  24041  dfrtrcl2  24060  eldm3  24190  funsseq  24196  wfr3g  24326  wfrlem1  24327  wfrlem4  24330  wfrlem14  24340  wfr2  24344  wfr2c  24345  tfrALTlem  24347  tfr2ALT  24349  tfr3ALT  24350  frr3g  24351  frrlem1  24352  frrlem4  24355  bpolylem  24855  bpolyval  24856  domrancur1b  25303  domrancur1c  25305  valcurfn1  25307  isprsr  25327  preoref12  25331  svs2  25590  svs3  25591  sdclem2  26555  prdsbnd2  26622  eldiophb  26939  diophrw  26941  diophin  26955  sblpnf  27642  funcoressn  28095  bnj1385  29181  bnj1326  29372  bnj1321  29373  bnj1442  29395  bnj1450  29396  bnj1463  29401  bnj1529  29416  dibffval  31952  hdmapffval  32641  hdmapfval  32642
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-opab 4094  df-xp 4711  df-res 4717
  Copyright terms: Public domain W3C validator