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

Theorem reseq1d 4970
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 4965 . 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 1632    |` cres 4707
This theorem is referenced by:  reseq12d  4972  fun2ssres  5311  funcnvres2  5339  fresin  5426  fresaunres2  5429  offres  6108  itunifval  8058  hsmex  8074  gruima  8440  fseq1p1m1  10873  ltweuz  11040  rlimres  12048  lo1res  12049  lo1resb  12054  rlimresb  12055  o1resb  12056  bitsf1ocnv  12651  setsres  13190  setscom  13192  sscres  13716  resfval2  13783  gsumzres  15210  gsumzsplit  15222  gsum2d  15239  dpjidcl  15309  pgpfaclem1  15332  znle2  16523  tmdgsum  17794  tsmsval2  17828  tsmsres  17842  tsmssplit  17850  imasdsf1olem  17953  tmslem  18044  sranlm  18211  srabn  18793  mbflimsup  19037  dvres  19277  dvres3a  19280  dvnres  19296  cpnres  19302  dvmulbr  19304  dvcmul  19309  dvcmulf  19310  dvcobr  19311  dvmptres3  19321  dvmptres2  19327  dvcnvlem  19339  dvlip2  19358  ftc2ditglem  19408  aannenlem1  19724  eff1olem  19926  resqrcn  20105  sqrcn  20106  rlimcnp2  20277  jensenlem2  20298  ex-res  20844  drngoi  21090  indf1ofs  23624  cvmliftlem10  23840  cvmlift2lem6  23854  cvmlift2lem12  23860  trpredeq1  24294  trpredeq2  24295  trpredeq3  24296  itgaddnclem2  25010  valtar  25986  trclval  25997  cocnv  26496  cnpwstotbnd  26624  eldioph2  26944  pwssplit2  27292  pwssplit3  27293  psgnunilem5  27520  dvsconst  27650  cncfmptss  27820  itgsinexplem1  27851
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-res 4717
  Copyright terms: Public domain W3C validator