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

Theorem reseq1d 5145
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 5140 . 2  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    |` cres 4880
This theorem is referenced by:  reseq12d  5147  fun2ssres  5494  funcnvres2  5524  fresin  5612  fresaunres2  5615  offres  6319  itunifval  8296  hsmex  8312  gruima  8677  fseq1p1m1  11122  ltweuz  11301  rlimres  12352  lo1res  12353  lo1resb  12358  rlimresb  12359  o1resb  12360  bitsf1ocnv  12956  setsres  13495  setscom  13497  sscres  14023  resfval2  14090  gsumzres  15517  gsumzsplit  15529  gsum2d  15546  dpjidcl  15616  pgpfaclem1  15639  znle2  16834  tmdgsum  18125  tsmsval2  18159  tsmsres  18173  tsmssplit  18181  imasdsf1olem  18403  tmslem  18512  sranlm  18720  srabn  19314  mbflimsup  19558  dvres  19798  dvres3a  19801  dvnres  19817  cpnres  19823  dvcmul  19830  dvcmulf  19831  dvcobr  19832  dvmptres3  19842  dvmptres2  19848  dvcnvlem  19860  dvlip2  19879  ftc2ditglem  19929  aannenlem1  20245  eff1olem  20450  resqrcn  20633  sqrcn  20634  rlimcnp2  20805  jensenlem2  20826  ex-res  21749  drngoi  21995  zhmnrg  24351  indf1ofs  24423  cvmliftlem10  24981  cvmlift2lem6  24995  cvmlift2lem12  25001  trpredeq1  25498  trpredeq2  25499  trpredeq3  25500  ftc1anclem8  26287  ftc2nc  26289  cocnv  26427  cnpwstotbnd  26506  eldioph2  26820  pwssplit2  27166  pwssplit3  27167  psgnunilem5  27394  dvsconst  27524  cncfmptss  27693  itgsinexplem1  27724
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 2958  df-in 3327  df-res 4890
  Copyright terms: Public domain W3C validator