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

Theorem reseq1d 5112
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 5107 . 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 1369    |` cres 4845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338  df-res 4855
This theorem is referenced by:  reseq12d  5114  fun2ssres  5462  funcnvres2  5492  fresin  5583  fresaunres2  5586  offres  6575  itunifval  8588  hsmex  8604  gruima  8972  fseq1p1m1  11537  ltweuz  11787  rlimres  13039  lo1res  13040  lo1resb  13045  rlimresb  13046  o1resb  13047  bitsf1ocnv  13643  fsets  14203  setsres  14205  setscom  14207  sscres  14739  resfval2  14806  psgnunilem5  16003  gsumzres  16391  gsumzresOLD  16395  gsumzsplit  16421  gsumzsplitOLD  16422  gsum2dlem2  16465  gsum2dOLD  16467  dpjidcl  16560  dpjidclOLD  16567  pgpfaclem1  16585  pwssplit2  17144  pwssplit3  17145  znle2  17989  mamures  18293  ofco2  18335  mdetunilem9  18429  mdetmul  18432  smadiadetglem1  18480  smadiadetglem2  18481  tmdgsum  19669  tsmsval2  19703  tsmsresOLD  19720  tsmsres  19721  tsmssplit  19729  imasdsf1olem  19951  tmslem  20060  sranlm  20268  srabn  20875  mbflimsup  21147  dvres  21389  dvres3a  21392  dvnres  21408  cpnres  21414  dvcmul  21421  dvcmulf  21422  dvcobr  21423  dvmptres3  21433  dvmptres2  21439  dvcnvlem  21451  dvlip2  21470  ftc2ditglem  21520  aannenlem1  21797  eff1olem  22007  resqrcn  22190  sqrcn  22191  rlimcnp2  22363  jensenlem2  22384  ex-res  23651  drngoi  23897  resf1o  26033  zhmnrg  26399  indf1ofs  26485  fibp1  26787  cvmliftlem10  27186  cvmlift2lem6  27200  cvmlift2lem12  27206  trpredeq1  27687  trpredeq2  27688  trpredeq3  27689  ftc1anclem8  28477  ftc2nc  28479  cocnv  28622  cnpwstotbnd  28699  eldioph2  29103  itgpowd  29593  dvsconst  29607  cncfmptss  29771  itgsinexplem1  29797
  Copyright terms: Public domain W3C validator