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

Theorem reseq2d 5086
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 5081 . 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 1649    |` cres 4820
This theorem is referenced by:  reseq12d  5087  resima2  5119  relresfld  5336  f1orescnv  5630  funcocnv2  5640  fococnv2  5641  fnressn  5857  fnsnsplit  5869  oprssov  6154  curry1  6377  curry2  6380  dftpos2  6432  tfrlem16  6590  sbthlem4  7156  mapunen  7212  hartogslem1  7444  axdc3lem2  8264  fseq1p1m1  11052  hashf1lem1  11631  setsval  13420  idfuval  14000  idfu2nd  14001  resf1st  14018  setcid  14168  catcisolem  14188  1stfval  14215  1stf2  14217  2ndfval  14218  2ndf2  14220  1stfcl  14221  2ndfcl  14222  curf2ndf  14271  hofcl  14283  isps  14561  cnvps  14571  isdir  14604  dirref  14607  tsrdir  14610  frmdval  14723  frmdplusg  14726  gsum2d  15473  dprd2da  15527  dpjval  15541  ablfac1eulem  15557  ablfac1eu  15558  psrplusg  16372  opsrtoslem2  16472  imacmp  17382  ptuncnv  17760  tgphaus  18067  tsmsres  18094  tsmsxplem1  18103  tsmsxplem2  18104  trust  18180  metreslem  18300  imasdsf1olem  18311  xmspropd  18393  mspropd  18394  imasf1oxms  18409  imasf1oms  18410  nmpropd2  18513  isngp2  18515  ngppropd  18549  tngngp2  18564  cmspropd  19171  mbfres2  19404  limciun  19648  dvmptres3  19709  dvmptres2  19715  dvmptntr  19724  dvlipcn  19745  dvlip2  19746  c1liplem1  19747  dvgt0lem1  19753  lhop1lem  19764  dvcnvrelem1  19768  dvcvx  19771  ftc2ditglem  19796  wilthlem2  20719  dchrval  20885  dchrelbas2  20888  1pthonlem1  21437  eupath2lem3  21549  eupath2  21550  efghgrp  21809  drngoi  21843  isdivrngo  21867  hhssablo  22611  hhssnvt  22613  hhsssh  22617  esumcvg  24272  cvmliftlem5  24755  cvmliftlem7  24757  cvmliftlem10  24760  cvmliftlem11  24761  cvmliftlem15  24764  cvmlift2lem11  24779  cvmlift2lem12  24780  ghomgrplem  24879  relexp0  24908  relexpsucr  24909  dfrtrcl2  24927  eldm3  25143  funsseq  25149  wfr3g  25279  wfrlem1  25280  wfrlem4  25283  wfrlem14  25293  wfr2  25297  wfr2c  25298  tfrALTlem  25300  tfr2ALT  25302  tfr3ALT  25303  frr3g  25304  frrlem1  25305  frrlem4  25308  bpolylem  25808  bpolyval  25809  sdclem2  26137  prdsbnd2  26195  eldiophb  26506  diophrw  26508  diophin  26522  sblpnf  27208  funcoressn  27660  bnj1385  28542  bnj1326  28733  bnj1321  28734  bnj1442  28756  bnj1450  28757  bnj1463  28762  bnj1529  28777  dibffval  31255  hdmapffval  31944  hdmapfval  31945
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 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-v 2901  df-in 3270  df-opab 4208  df-xp 4824  df-res 4830
  Copyright terms: Public domain W3C validator