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

Theorem reseq1d 5502
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 5497 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  cres 5220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-in 3687  df-res 5230
This theorem is referenced by:  reseq12d  5504  fun2ssres  6044  funcnvres2  6082  fresin  6186  fresaunres2  6189  offres  7280  itunifval  9351  hsmex  9367  gruima  9737  fseq1p1m1  12528  ltweuz  12875  rlimres  14409  lo1res  14410  lo1resb  14415  rlimresb  14416  o1resb  14417  bitsf1ocnv  15289  fsets  16014  setsres  16024  setscom  16026  sscres  16605  resfval2  16675  estrres  16901  psgnunilem5  18035  gsumzres  18431  gsumzsplit  18448  gsum2dlem2  18491  dpjidcl  18578  pgpfaclem1  18601  pwssplit2  19183  pwssplit3  19184  znle2  20025  phssip  20126  mamures  20319  ofco2  20380  mdetunilem9  20549  mdetmul  20552  smadiadetglem1  20600  smadiadetglem2  20601  tmdgsum  22021  tsmsval2  22055  tsmsres  22069  tsmssplit  22077  imasdsf1olem  22300  tmslem  22409  sranlm  22610  srabn  23277  mbflimsup  23553  dvres  23795  dvres3a  23798  dvnres  23814  cpnres  23820  dvcmul  23827  dvcmulf  23828  dvcobr  23829  dvmptres3  23839  dvmptres2  23845  dvcnvlem  23859  dvlip2  23878  ftc2ditglem  23928  aannenlem1  24203  eff1olem  24414  resqrtcn  24610  sqrtcn  24611  rlimcnp2  24813  jensenlem2  24834  ex-res  27530  rabfodom  29572  resf1o  29735  submatres  30102  zhmnrg  30241  indf1ofs  30318  carsggect  30610  fibp1  30693  actfunsnf1o  30912  cvmliftlem10  31504  cvmlift2lem6  31518  cvmlift2lem12  31524  trpredeq1  31946  trpredeq2  31947  trpredeq3  31948  poimirlem3  33644  ftc1anclem8  33724  ftc2nc  33726  cocnv  33752  cnpwstotbnd  33828  drngoi  33982  eldioph2  37744  itgpowd  38219  dvsconst  38948  disjf1o  39794  cncfmptss  40239  limsupresuz  40355  liminfresuz  40436  dvmptresicc  40554  itgsinexplem1  40589  itgcoscmulx  40605  itgiccshift  40616  itgperiod  40617  dirkeritg  40739  dirkercncflem2  40741  dirkercncflem4  40743  fourierdlem16  40760  fourierdlem21  40765  fourierdlem22  40766  fourierdlem28  40772  fourierdlem42  40786  fourierdlem78  40821  fourierdlem81  40824  fourierdlem83  40826  fourierdlem84  40827  fourierdlem90  40833  fourierdlem93  40836  fourierdlem103  40846  fourierdlem104  40847  sge0resrnlem  41040  ismeannd  41104  0ome  41166  hoidmvlelem3  41234  hoidmvlelem4  41235  funcrngcsetc  42425  funcringcsetc  42462  rhmsubclem1  42513  rhmsubcALTVlem1  42531  aacllem  42977
  Copyright terms: Public domain W3C validator