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

Theorem reseq1d 5261
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 5256 . 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 1398    |` cres 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-res 5000
This theorem is referenced by:  reseq12d  5263  fun2ssres  5611  funcnvres2  5641  fresin  5736  fresaunres2  5739  offres  6768  itunifval  8787  hsmex  8803  gruima  9169  fseq1p1m1  11756  ltweuz  12054  rlimres  13463  lo1res  13464  lo1resb  13469  rlimresb  13470  o1resb  13471  bitsf1ocnv  14178  fsets  14744  setsres  14746  setscom  14748  sscres  15311  resfval2  15381  estrres  15607  psgnunilem5  16718  gsumzres  17113  gsumzresOLD  17117  gsumzsplit  17143  gsumzsplitOLD  17144  gsum2dlem2  17194  gsum2dOLD  17196  dpjidcl  17302  dpjidclOLD  17309  pgpfaclem1  17327  pwssplit2  17901  pwssplit3  17902  znle2  18765  mamures  19059  ofco2  19120  mdetunilem9  19289  mdetmul  19292  smadiadetglem1  19340  smadiadetglem2  19341  tmdgsum  20760  tsmsval2  20794  tsmsresOLD  20811  tsmsres  20812  tsmssplit  20820  imasdsf1olem  21042  tmslem  21151  sranlm  21359  srabn  21966  mbflimsup  22239  dvres  22481  dvres3a  22484  dvnres  22500  cpnres  22506  dvcmul  22513  dvcmulf  22514  dvcobr  22515  dvmptres3  22525  dvmptres2  22531  dvcnvlem  22543  dvlip2  22562  ftc2ditglem  22612  aannenlem1  22890  eff1olem  23101  resqrtcn  23291  sqrtcn  23292  rlimcnp2  23494  jensenlem2  23515  ex-res  25364  drngoi  25607  rabfodom  27603  resf1o  27784  zhmnrg  28182  indf1ofs  28255  carsggect  28526  fibp1  28604  cvmliftlem10  29003  cvmlift2lem6  29017  cvmlift2lem12  29023  trpredeq1  29543  trpredeq2  29544  trpredeq3  29545  ftc1anclem8  30337  ftc2nc  30339  cocnv  30456  cnpwstotbnd  30533  eldioph2  30934  itgpowd  31423  dvsconst  31476  cncfmptss  31820  dvmptresicc  31955  itgsinexplem1  31991  itgcoscmulx  32007  itgiccshift  32018  itgperiod  32019  dirkeritg  32123  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem16  32144  fourierdlem21  32149  fourierdlem22  32150  fourierdlem28  32156  fourierdlem42  32170  fourierdlem78  32206  fourierdlem81  32209  fourierdlem83  32211  fourierdlem84  32212  fourierdlem90  32218  fourierdlem93  32221  fourierdlem103  32231  fourierdlem104  32232  funcrngcsetc  33060  funcringcsetc  33097  rhmsubclem1  33148  rhmsubcALTVlem1  33167  aacllem  33604
  Copyright terms: Public domain W3C validator