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

Theorem reseq1i 5424
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 5422 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:   = 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:  reseq12i  5426  resindm  5479  resmpt  5484  resmpt3  5485  resmptf  5486  opabresid  5490  rescnvcnv  5632  coires1  5691  fresaunres1  6115  fcoi1  6116  fninfp  6481  fvsnun1  6489  fvsnun2  6490  resoprab  6798  resmpt2  6800  elrnmpt2res  6816  ofmres  7206  f1stres  7234  f2ndres  7235  df1st2  7308  df2nd2  7309  dftpos2  7414  wfrlem14  7473  tfr2a  7536  tfr2b  7537  rdgseg  7563  frsucmpt2  7580  seqomlem2  7591  seqomlem3  7592  seqomlem4  7593  domss2  8160  dffi3  8378  fpwwe2lem13  9502  seqval  12852  hashgval  13160  hashinf  13162  pgrpsubgsymg  17874  gsumzunsnd  18401  ablfac1b  18515  zzngim  19949  pmatcollpw3lem  20636  cnmptid  21512  txflf  21857  xmsxmet2  22311  msmet2  22312  tmsxpsmopn  22389  isngp2  22448  subgnm  22484  tngngp2  22503  cnfldms  22626  msdcn  22691  oprpiece1res1  22797  oprpiece1res2  22798  isncvsngp  22995  cncms  23197  cnfldcusp  23199  reust  23215  minveclem3a  23244  dvreslem  23718  dvres2lem  23719  dvcmulf  23753  mdegfval  23867  psercn  24225  abelth  24240  efcvx  24248  efifo  24338  dfrelog  24357  dvrelog  24428  dvlog  24442  efopnlem2  24448  dvatan  24707  dchrisumlem1  25223  elimampt  29566  df1stres  29609  df2ndres  29610  padct  29625  ressplusf  29778  ressnm  29779  gsummpt2d  29909  qqhcn  30163  cnrrext  30182  rrhre  30193  esumcvg  30276  dya2icoseg2  30468  eulerpartgbij  30562  trpred0  31860  noetalem2  31989  noetalem3  31990  neibastop2  32481  mptsnunlem  33315  icorempt2  33329  poimirlem3  33542  mbfposadd  33587  ftc1anclem3  33617  dvasin  33626  dvacos  33627  prdsbnd2  33724  repwsmet  33763  rrnequiv  33764  inres2  34150  xrnres  34300  xrnres2  34301  xrnres3  34302  diophin  37653  eldioph4b  37692  dnnumch1  37931  aomclem6  37946  radcnvrat  38830  lhe4.4ex1a  38845  dvsid  38847  dvsef  38848  imassmpt  39795  elicores  40078  climresmpt  40209  dvcosre  40444  dvmptresicc  40452  itgsinexplem1  40487  fourierdlem40  40682  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem80  40721  fourierdlem84  40725  fourierdlem85  40726  fourierdlem101  40742  fourierdlem102  40743  fourierdlem111  40752  fourierdlem114  40755  fouriersw  40766  fouriercn  40767  volicorescl  41088  fdmdifeqresdif  42445  aacllem  42875
  Copyright terms: Public domain W3C validator