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

Theorem reseq1d 5846
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
reseq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem reseq1d
StepHypRef Expression
1 reseqd.1 . 2 (𝜑𝐴 = 𝐵)
2 reseq1 5841 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  cres 5551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942  df-res 5561
This theorem is referenced by:  reseq12d  5848  fun2ssres  6393  funcnvres2  6428  fresin  6541  fresaunres2  6544  offres  7678  itunifval  9832  hsmex  9848  gruima  10218  fseq1p1m1  12975  ltweuz  13323  rlimres  14909  lo1res  14910  lo1resb  14915  rlimresb  14916  o1resb  14917  bitsf1ocnv  15787  fsets  16510  setsres  16519  setscom  16521  sscres  17087  resfval2  17157  estrres  17383  symgvalstruct  18519  gsumzres  19023  gsumzsplit  19041  gsum2dlem2  19085  dpjidcl  19174  pgpfaclem1  19197  pwssplit2  19826  pwssplit3  19827  znle2  20694  phssip  20796  mamures  20995  ofco2  21054  mdetunilem9  21223  mdetmul  21226  smadiadetglem1  21274  smadiadetglem2  21275  tmdgsum  22697  tsmsval2  22732  tsmsres  22746  tsmssplit  22754  imasdsf1olem  22977  tmslem  23086  sranlm  23287  cmssmscld  23947  srabn  23957  cmscsscms  23970  mbflimsup  24261  dvres  24503  dvres3a  24506  dvnres  24522  cpnres  24528  dvcmul  24535  dvcmulf  24536  dvcobr  24537  dvmptres3  24547  dvmptres2  24553  dvcnvlem  24567  dvlip2  24586  ftc2ditglem  24636  aannenlem1  24911  eff1olem  25126  resqrtcn  25324  sqrtcn  25325  rlimcnp2  25538  jensenlem2  25559  ex-res  28214  rabfodom  30260  resf1o  30460  tocycfvres1  30747  tocycfvres2  30748  cycpmconjvlem  30778  cycpmconjslem2  30792  cyc3conja  30794  lbsdiflsp0  31017  submatres  31066  zhmnrg  31203  indf1ofs  31280  carsggect  31571  fibp1  31654  actfunsnf1o  31870  cvmliftlem10  32536  cvmlift2lem6  32550  cvmlift2lem12  32556  satf  32595  trpredeq1  33054  trpredeq2  33055  trpredeq3  33056  poimirlem3  34889  ftc1anclem8  34968  ftc2nc  34970  cocnv  34994  cnpwstotbnd  35069  drngoi  35223  eldioph2  39352  itgpowd  39814  dvsconst  40655  disjf1o  41445  cncfmptss  41861  limsupresuz  41977  liminfresuz  42058  dvmptresicc  42197  itgsinexplem1  42232  itgcoscmulx  42247  itgiccshift  42258  itgperiod  42259  dirkeritg  42381  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem16  42402  fourierdlem21  42407  fourierdlem22  42408  fourierdlem28  42414  fourierdlem42  42428  fourierdlem78  42463  fourierdlem81  42466  fourierdlem83  42468  fourierdlem84  42469  fourierdlem90  42475  fourierdlem93  42478  fourierdlem103  42488  fourierdlem104  42489  sge0resrnlem  42679  ismeannd  42743  0ome  42805  hoidmvlelem3  42873  hoidmvlelem4  42874  funcrngcsetc  44263  funcringcsetc  44300  rhmsubclem1  44351  rhmsubcALTVlem1  44369  aacllem  44896
  Copyright terms: Public domain W3C validator