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

Theorem reseq1d 5262
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 5257 . 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 1383    |` cres 4991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-res 5001
This theorem is referenced by:  reseq12d  5264  fun2ssres  5619  funcnvres2  5649  fresin  5744  fresaunres2  5747  offres  6780  itunifval  8799  hsmex  8815  gruima  9183  fseq1p1m1  11761  ltweuz  12051  rlimres  13360  lo1res  13361  lo1resb  13366  rlimresb  13367  o1resb  13368  bitsf1ocnv  13971  fsets  14535  setsres  14537  setscom  14539  sscres  15069  resfval2  15136  psgnunilem5  16393  gsumzres  16788  gsumzresOLD  16792  gsumzsplit  16818  gsumzsplitOLD  16819  gsum2dlem2  16872  gsum2dOLD  16874  dpjidcl  16981  dpjidclOLD  16988  pgpfaclem1  17006  pwssplit2  17580  pwssplit3  17581  znle2  18465  mamures  18765  ofco2  18826  mdetunilem9  18995  mdetmul  18998  smadiadetglem1  19046  smadiadetglem2  19047  tmdgsum  20467  tsmsval2  20501  tsmsresOLD  20518  tsmsres  20519  tsmssplit  20527  imasdsf1olem  20749  tmslem  20858  sranlm  21066  srabn  21673  mbflimsup  21946  dvres  22188  dvres3a  22191  dvnres  22207  cpnres  22213  dvcmul  22220  dvcmulf  22221  dvcobr  22222  dvmptres3  22232  dvmptres2  22238  dvcnvlem  22250  dvlip2  22269  ftc2ditglem  22319  aannenlem1  22596  eff1olem  22807  resqrtcn  22995  sqrtcn  22996  rlimcnp2  23168  jensenlem2  23189  ex-res  25034  drngoi  25281  rabfodom  27276  resf1o  27425  zhmnrg  27821  indf1ofs  27912  fibp1  28213  cvmliftlem10  28612  cvmlift2lem6  28626  cvmlift2lem12  28632  trpredeq1  29278  trpredeq2  29279  trpredeq3  29280  ftc1anclem8  30072  ftc2nc  30074  cocnv  30191  cnpwstotbnd  30268  eldioph2  30670  itgpowd  31158  dvsconst  31211  cncfmptss  31509  dvmptresicc  31620  itgsinexplem1  31642  itgcoscmulx  31658  itgiccshift  31669  itgperiod  31670  dirkeritg  31773  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem16  31794  fourierdlem21  31799  fourierdlem22  31800  fourierdlem28  31806  fourierdlem42  31820  fourierdlem78  31856  fourierdlem81  31859  fourierdlem83  31861  fourierdlem84  31862  fourierdlem90  31868  fourierdlem93  31871  fourierdlem103  31881  fourierdlem104  31882  estrres  32491  funcrngcsetc  32542  funcringcsetc  32575  rhmsubclem1  32622  rhmsubcOLDlem1  32641
  Copyright terms: Public domain W3C validator