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

Theorem reseq1d 5427
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 5422 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cres 5145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-res 5155
This theorem is referenced by:  reseq12d  5429  fun2ssres  5969  funcnvres2  6007  fresin  6111  fresaunres2  6114  offres  7205  itunifval  9276  hsmex  9292  gruima  9662  fseq1p1m1  12452  ltweuz  12800  rlimres  14333  lo1res  14334  lo1resb  14339  rlimresb  14340  o1resb  14341  bitsf1ocnv  15213  fsets  15938  setsres  15948  setscom  15950  sscres  16530  resfval2  16600  estrres  16826  psgnunilem5  17960  gsumzres  18356  gsumzsplit  18373  gsum2dlem2  18416  dpjidcl  18503  pgpfaclem1  18526  pwssplit2  19108  pwssplit3  19109  znle2  19950  phssip  20051  mamures  20244  ofco2  20305  mdetunilem9  20474  mdetmul  20477  smadiadetglem1  20525  smadiadetglem2  20526  tmdgsum  21946  tsmsval2  21980  tsmsres  21994  tsmssplit  22002  imasdsf1olem  22225  tmslem  22334  sranlm  22535  srabn  23202  mbflimsup  23478  dvres  23720  dvres3a  23723  dvnres  23739  cpnres  23745  dvcmul  23752  dvcmulf  23753  dvcobr  23754  dvmptres3  23764  dvmptres2  23770  dvcnvlem  23784  dvlip2  23803  ftc2ditglem  23853  aannenlem1  24128  eff1olem  24339  resqrtcn  24535  sqrtcn  24536  rlimcnp2  24738  jensenlem2  24759  ex-res  27428  rabfodom  29470  resf1o  29633  submatres  30000  zhmnrg  30139  indf1ofs  30216  carsggect  30508  fibp1  30591  actfunsnf1o  30810  cvmliftlem10  31402  cvmlift2lem6  31416  cvmlift2lem12  31422  trpredeq1  31844  trpredeq2  31845  trpredeq3  31846  poimirlem3  33542  ftc1anclem8  33622  ftc2nc  33624  cocnv  33650  cnpwstotbnd  33726  drngoi  33880  eldioph2  37642  itgpowd  38117  dvsconst  38846  disjf1o  39692  cncfmptss  40137  limsupresuz  40253  liminfresuz  40334  dvmptresicc  40452  itgsinexplem1  40487  itgcoscmulx  40503  itgiccshift  40514  itgperiod  40515  dirkeritg  40637  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem28  40670  fourierdlem42  40684  fourierdlem78  40719  fourierdlem81  40722  fourierdlem83  40724  fourierdlem84  40725  fourierdlem90  40731  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  sge0resrnlem  40938  ismeannd  41002  0ome  41064  hoidmvlelem3  41132  hoidmvlelem4  41133  funcrngcsetc  42323  funcringcsetc  42360  rhmsubclem1  42411  rhmsubcALTVlem1  42429  aacllem  42875
  Copyright terms: Public domain W3C validator