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

Theorem reseq1d 5263
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 5258 . 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 1374    |` cres 4994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-res 5004
This theorem is referenced by:  reseq12d  5265  fun2ssres  5620  funcnvres2  5650  fresin  5745  fresaunres2  5748  offres  6769  itunifval  8785  hsmex  8801  gruima  9169  fseq1p1m1  11741  ltweuz  12028  rlimres  13330  lo1res  13331  lo1resb  13336  rlimresb  13337  o1resb  13338  bitsf1ocnv  13942  fsets  14505  setsres  14507  setscom  14509  sscres  15042  resfval2  15109  psgnunilem5  16308  gsumzres  16698  gsumzresOLD  16702  gsumzsplit  16728  gsumzsplitOLD  16729  gsum2dlem2  16782  gsum2dOLD  16784  dpjidcl  16890  dpjidclOLD  16897  pgpfaclem1  16915  pwssplit2  17482  pwssplit3  17483  znle2  18352  mamures  18652  ofco2  18713  mdetunilem9  18882  mdetmul  18885  smadiadetglem1  18933  smadiadetglem2  18934  tmdgsum  20322  tsmsval2  20356  tsmsresOLD  20373  tsmsres  20374  tsmssplit  20382  imasdsf1olem  20604  tmslem  20713  sranlm  20921  srabn  21528  mbflimsup  21801  dvres  22043  dvres3a  22046  dvnres  22062  cpnres  22068  dvcmul  22075  dvcmulf  22076  dvcobr  22077  dvmptres3  22087  dvmptres2  22093  dvcnvlem  22105  dvlip2  22124  ftc2ditglem  22174  aannenlem1  22451  eff1olem  22661  resqrcn  22844  sqrcn  22845  rlimcnp2  23017  jensenlem2  23038  ex-res  24825  drngoi  25071  resf1o  27211  zhmnrg  27570  indf1ofs  27665  fibp1  27966  cvmliftlem10  28365  cvmlift2lem6  28379  cvmlift2lem12  28385  trpredeq1  28866  trpredeq2  28867  trpredeq3  28868  ftc1anclem8  29661  ftc2nc  29663  cocnv  29806  cnpwstotbnd  29883  eldioph2  30286  itgpowd  30776  dvsconst  30790  cncfmptss  31092  dvmptresicc  31204  itgsinexplem1  31226  itgcoscmulx  31242  itgiccshift  31253  itgperiod  31254  dirkeritg  31357  dirkercncflem2  31359  dirkercncflem4  31361  fourierdlem16  31378  fourierdlem21  31383  fourierdlem22  31384  fourierdlem28  31390  fourierdlem42  31404  fourierdlem78  31440  fourierdlem81  31443  fourierdlem83  31445  fourierdlem84  31446  fourierdlem90  31452  fourierdlem93  31455  fourierdlem103  31465  fourierdlem104  31466
  Copyright terms: Public domain W3C validator