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

Theorem reseq1i 5847
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypothesis
Ref Expression
reseqi.1 𝐴 = 𝐵
Assertion
Ref Expression
reseq1i (𝐴𝐶) = (𝐵𝐶)

Proof of Theorem reseq1i
StepHypRef Expression
1 reseqi.1 . 2 𝐴 = 𝐵
2 reseq1 5845 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cres 5555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-rab 3151  df-in 3946  df-res 5565
This theorem is referenced by:  reseq12i  5849  resindm  5898  resmpt  5903  resmpt3  5904  resmptf  5905  opabresid  5915  opabresidOLD  5917  rescnvcnv  6058  coires1  6114  fresaunres1  6547  fcoi1  6548  fninfp  6931  fvsnun1  6941  fvsnun2  6942  fvsnun1OLD  6943  fvsnun2OLD  6944  resoprab  7263  resmpo  7265  elrnmpores  7281  ofmres  7679  f1stres  7707  f2ndres  7708  df1st2  7787  df2nd2  7788  fsplitfpar  7808  dftpos2  7903  wfrlem14  7962  tfr2a  8025  tfr2b  8026  rdgseg  8052  frsucmpt2w  8069  frsucmpt2  8070  seqomlem2  8081  seqomlem3  8082  seqomlem4  8083  domss2  8668  dffi3  8887  fpwwe2lem13  10056  seqval  13373  hashgval  13686  hashinf  13688  pgrpsubgsymg  18458  gsumzunsnd  18998  ablfac1b  19114  zzngim  20615  pmatcollpw3lem  21307  txflf  22530  xmsxmet2  22984  msmet2  22985  tmsxpsmopn  23062  isngp2  23121  subgnm  23157  tngngp2  23176  cnfldms  23299  msdcn  23364  oprpiece1res1  23470  oprpiece1res2  23471  isncvsngp  23668  cncms  23873  cnfldcusp  23875  reust  23899  minveclem3a  23945  dvreslem  24422  dvres2lem  24423  dvcmulf  24457  mdegfval  24571  psercn  24929  abelth  24944  efcvx  24952  efifo  25044  dfrelog  25062  dvrelog  25133  dvlog  25147  efopnlem2  25153  dvatan  25426  dchrisumlem1  25979  wlknwwlksnbij  27580  elimampt  30298  fnunres2  30339  df1stres  30352  df2ndres  30353  padct  30368  ressplusf  30551  ressnm  30552  gsummpt2d  30601  cycpmrn  30699  tocyccntz  30700  cycpmconjslem2  30711  qqhcn  31118  cnrrext  31137  rrhre  31148  esumcvg  31231  dya2icoseg2  31422  eulerpartgbij  31516  satf0  32503  trpred0  32959  frrlem12  33018  noetalem2  33102  noetalem3  33103  neibastop2  33593  mptsnunlem  34488  icorempo  34501  poimirlem3  34762  mbfposadd  34806  ftc1anclem3  34836  dvasin  34845  dvacos  34846  prdsbnd2  34941  repwsmet  34980  rrnequiv  34981  inres2  35374  xrnres  35517  xrnres2  35518  xrnres3  35519  diophin  39230  eldioph4b  39269  dnnumch1  39505  aomclem6  39520  radcnvrat  40507  lhe4.4ex1a  40522  dvsid  40524  dvsef  40525  imassmpt  41398  elicores  41670  climresmpt  41801  dvcosre  42057  dvmptresicc  42065  itgsinexplem1  42100  fourierdlem40  42294  fourierdlem57  42310  fourierdlem58  42311  fourierdlem62  42315  fourierdlem74  42327  fourierdlem75  42328  fourierdlem76  42329  fourierdlem80  42333  fourierdlem84  42337  fourierdlem85  42338  fourierdlem101  42354  fourierdlem102  42355  fourierdlem111  42364  fourierdlem114  42367  fouriersw  42378  fouriercn  42379  volicorescl  42697  fdmdifeqresdif  44218  aacllem  44730
  Copyright terms: Public domain W3C validator