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

Theorem reseq1d 5101
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
reseq1d  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )

Proof of Theorem reseq1d
StepHypRef Expression
1 reseqd.1 . 2  |-  ( ph  ->  A  =  B )
2 reseq1 5096 . 2  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    |` cres 4834
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2968  df-in 3328  df-res 4844
This theorem is referenced by:  reseq12d  5103  fun2ssres  5452  funcnvres2  5482  fresin  5573  fresaunres2  5576  offres  6567  itunifval  8577  hsmex  8593  gruima  8961  fseq1p1m1  11526  ltweuz  11776  rlimres  13028  lo1res  13029  lo1resb  13034  rlimresb  13035  o1resb  13036  bitsf1ocnv  13632  fsets  14192  setsres  14194  setscom  14196  sscres  14728  resfval2  14795  psgnunilem5  15989  gsumzres  16377  gsumzresOLD  16381  gsumzsplit  16407  gsumzsplitOLD  16408  gsum2dlem2  16448  gsum2dOLD  16450  dpjidcl  16543  dpjidclOLD  16550  pgpfaclem1  16568  pwssplit2  17115  pwssplit3  17116  znle2  17955  mamures  18259  ofco2  18301  mdetunilem9  18395  mdetmul  18398  smadiadetglem1  18446  smadiadetglem2  18447  tmdgsum  19635  tsmsval2  19669  tsmsresOLD  19686  tsmsres  19687  tsmssplit  19695  imasdsf1olem  19917  tmslem  20026  sranlm  20234  srabn  20841  mbflimsup  21113  dvres  21355  dvres3a  21358  dvnres  21374  cpnres  21380  dvcmul  21387  dvcmulf  21388  dvcobr  21389  dvmptres3  21399  dvmptres2  21405  dvcnvlem  21417  dvlip2  21436  ftc2ditglem  21486  aannenlem1  21763  eff1olem  21973  resqrcn  22156  sqrcn  22157  rlimcnp2  22329  jensenlem2  22350  ex-res  23593  drngoi  23839  resf1o  25975  zhmnrg  26344  indf1ofs  26430  fibp1  26732  cvmliftlem10  27131  cvmlift2lem6  27145  cvmlift2lem12  27151  trpredeq1  27631  trpredeq2  27632  trpredeq3  27633  ftc1anclem8  28417  ftc2nc  28419  cocnv  28562  cnpwstotbnd  28639  eldioph2  29043  itgpowd  29533  dvsconst  29547  cncfmptss  29711  itgsinexplem1  29737
  Copyright terms: Public domain W3C validator