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

Theorem reseq2d 5139
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 5134 . 2  |-  ( A  =  B  ->  ( C  |`  A )  =  ( C  |`  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  |`  A )  =  ( C  |`  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    |` cres 4873
This theorem is referenced by:  reseq12d  5140  resima2  5172  relresfld  5389  f1orescnv  5683  funcocnv2  5693  fococnv2  5694  fnressn  5911  fnsnsplit  5923  oprssov  6208  curry1  6431  curry2  6434  dftpos2  6489  tfrlem16  6647  sbthlem4  7213  mapunen  7269  hartogslem1  7504  axdc3lem2  8324  fseq1p1m1  11115  hashf1lem1  11697  setsval  13486  idfuval  14066  idfu2nd  14067  resf1st  14084  setcid  14234  catcisolem  14254  1stfval  14281  1stf2  14283  2ndfval  14284  2ndf2  14286  1stfcl  14287  2ndfcl  14288  curf2ndf  14337  hofcl  14349  isps  14627  cnvps  14637  isdir  14670  dirref  14673  tsrdir  14676  frmdval  14789  frmdplusg  14792  gsum2d  15539  dprd2da  15593  dpjval  15607  ablfac1eulem  15623  ablfac1eu  15624  psrplusg  16438  opsrtoslem2  16538  imacmp  17453  ptuncnv  17832  tgphaus  18139  tsmsres  18166  tsmsxplem1  18175  tsmsxplem2  18176  trust  18252  metreslem  18385  imasdsf1olem  18396  xmspropd  18496  mspropd  18497  imasf1oxms  18512  imasf1oms  18513  nmpropd2  18635  isngp2  18637  ngppropd  18671  tngngp2  18686  cmspropd  19295  mbfres2  19530  limciun  19774  dvmptres3  19835  dvmptres2  19841  dvmptntr  19850  dvlipcn  19871  dvlip2  19872  c1liplem1  19873  dvgt0lem1  19879  lhop1lem  19890  dvcnvrelem1  19894  dvcvx  19897  ftc2ditglem  19922  wilthlem2  20845  dchrval  21011  dchrelbas2  21014  1pthonlem1  21582  constr2pth  21594  eupath2lem3  21694  eupath2  21695  efghgrp  21954  drngoi  21988  isdivrngo  22012  hhssablo  22756  hhssnvt  22758  hhsssh  22762  esumcvg  24469  cvmliftlem5  24969  cvmliftlem7  24971  cvmliftlem10  24974  cvmliftlem11  24975  cvmliftlem15  24978  cvmlift2lem11  24993  cvmlift2lem12  24994  ghomgrplem  25093  relexp0  25122  relexpsucr  25123  dfrtrcl2  25141  eldm3  25378  funsseq  25386  wrecseq123  25525  wfr3g  25530  wfrlem1  25531  wfrlem4  25534  wfrlem14  25544  wfr2  25548  tfrALTlem  25550  tfr2ALT  25552  tfr3ALT  25553  frr3g  25574  frrlem1  25575  frrlem4  25578  bpolylem  26087  sdclem2  26438  prdsbnd2  26496  eldiophb  26807  diophrw  26809  diophin  26823  sblpnf  27508  funcoressn  27959  usgra2pthspth  28259  bnj1385  29142  bnj1326  29333  bnj1321  29334  bnj1442  29356  bnj1450  29357  bnj1463  29362  bnj1529  29377  dibffval  31876  hdmapffval  32565  hdmapfval  32566
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-in 3320  df-opab 4260  df-xp 4877  df-res 4883
  Copyright terms: Public domain W3C validator