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

Theorem reseq1d 4954
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 4949 . 2  |-  ( A  =  B  ->  ( A  |`  C )  =  ( B  |`  C ) )
31, 2syl 15 1  |-  ( ph  ->  ( A  |`  C )  =  ( B  |`  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    |` cres 4691
This theorem is referenced by:  reseq12d  4956  fun2ssres  5295  funcnvres2  5323  fresin  5410  fresaunres2  5413  offres  6092  itunifval  8042  hsmex  8058  gruima  8424  fseq1p1m1  10857  ltweuz  11024  rlimres  12032  lo1res  12033  lo1resb  12038  rlimresb  12039  o1resb  12040  bitsf1ocnv  12635  setsres  13174  setscom  13176  sscres  13700  resfval2  13767  gsumzres  15194  gsumzsplit  15206  gsum2d  15223  dpjidcl  15293  pgpfaclem1  15316  znle2  16507  tmdgsum  17778  tsmsval2  17812  tsmsres  17826  tsmssplit  17834  imasdsf1olem  17937  tmslem  18028  sranlm  18195  srabn  18777  mbflimsup  19021  dvres  19261  dvres3a  19264  dvnres  19280  cpnres  19286  dvmulbr  19288  dvcmul  19293  dvcmulf  19294  dvcobr  19295  dvmptres3  19305  dvmptres2  19311  dvcnvlem  19323  dvlip2  19342  ftc2ditglem  19392  aannenlem1  19708  eff1olem  19910  resqrcn  20089  sqrcn  20090  rlimcnp2  20261  jensenlem2  20282  ex-res  20828  drngoi  21074  indf1ofs  23609  cvmliftlem10  23825  cvmlift2lem6  23839  cvmlift2lem12  23845  trpredeq1  24223  trpredeq2  24224  trpredeq3  24225  valtar  25883  trclval  25894  cocnv  26393  cnpwstotbnd  26521  eldioph2  26841  pwssplit2  27189  pwssplit3  27190  psgnunilem5  27417  dvsconst  27547  cncfmptss  27717  itgsinexplem1  27748
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-res 4701
  Copyright terms: Public domain W3C validator