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

Theorem reseq2d 4955
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 4950 . 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 1623    |` cres 4691
This theorem is referenced by:  reseq12d  4956  resima2  4988  relresfld  5199  f1orescnv  5488  funcocnv2  5498  fococnv2  5499  fnressn  5705  fnsnsplit  5717  oprssov  5989  curry1  6210  curry2  6213  dftpos2  6251  tfrlem16  6409  sbthlem4  6974  mapunen  7030  hartogslem1  7257  axdc3lem2  8077  fseq1p1m1  10857  hashf1lem1  11393  setsval  13172  idfuval  13750  idfu2nd  13751  resf1st  13768  setcid  13918  catcisolem  13938  1stfval  13965  1stf2  13967  2ndfval  13968  2ndf2  13970  1stfcl  13971  2ndfcl  13972  curf2ndf  14021  hofcl  14033  isps  14311  cnvps  14321  isdir  14354  dirref  14357  tsrdir  14360  frmdval  14473  frmdplusg  14476  gsum2d  15223  dprd2da  15277  dpjval  15291  ablfac1eulem  15307  ablfac1eu  15308  psrplusg  16126  opsrtoslem2  16226  imacmp  17124  ptuncnv  17498  tgphaus  17799  tsmsres  17826  tsmsxplem1  17835  tsmsxplem2  17836  metreslem  17926  imasdsf1olem  17937  xmspropd  18019  mspropd  18020  imasf1oxms  18035  imasf1oms  18036  nmpropd2  18117  isngp2  18119  ngppropd  18153  tngngp2  18168  cmspropd  18771  mbfres2  19000  limciun  19244  dvmptres3  19305  dvmptres2  19311  dvmptntr  19320  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  dvgt0lem1  19349  lhop1lem  19360  dvcnvrelem1  19364  dvcvx  19367  ftc2ditglem  19392  wilthlem2  20307  dchrval  20473  dchrelbas2  20476  efghgrp  21040  drngoi  21074  isdivrngo  21098  hhssablo  21840  hhssnvt  21842  hhsssh  21846  cvmliftlem5  23231  cvmliftlem7  23233  cvmliftlem10  23236  cvmliftlem11  23237  cvmliftlem15  23240  cvmlift2lem11  23255  cvmlift2lem12  23256  eupath2lem3  23314  eupath2  23315  ghomgrplem  23407  relexp0  23436  relexpsucr  23437  dfrtrcl2  23456  eldm3  23530  funsseq  23536  wfr3g  23666  wfrlem1  23667  wfrlem4  23670  wfrlem14  23680  wfr2  23684  wfr2c  23685  tfrALTlem  23687  tfr2ALT  23689  tfr3ALT  23690  frr3g  23691  frrlem1  23692  frrlem4  23695  bpolylem  24194  bpolyval  24195  domrancur1b  24612  domrancur1c  24614  valcurfn1  24616  isprsr  24636  preoref12  24640  svs2  24899  svs3  24900  sdclem2  25864  prdsbnd2  25931  eldiophb  26248  diophrw  26250  diophin  26264  sblpnf  26951  funcoressn  27402  bnj1385  28238  bnj1326  28429  bnj1321  28430  bnj1442  28452  bnj1450  28453  bnj1463  28458  bnj1529  28473  dibffval  30703  hdmapffval  31392  hdmapfval  31393
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