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

Theorem reseq12i 5979
Description: Equality inference for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypotheses
Ref Expression
reseqi.1 𝐴 = 𝐵
reseqi.2 𝐶 = 𝐷
Assertion
Ref Expression
reseq12i (𝐴𝐶) = (𝐵𝐷)

Proof of Theorem reseq12i
StepHypRef Expression
1 reseqi.1 . . 3 𝐴 = 𝐵
21reseq1i 5977 . 2 (𝐴𝐶) = (𝐵𝐶)
3 reseqi.2 . . 3 𝐶 = 𝐷
43reseq2i 5978 . 2 (𝐵𝐶) = (𝐵𝐷)
52, 4eqtri 2760 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  cres 5678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955  df-opab 5211  df-xp 5682  df-res 5688
This theorem is referenced by:  cnvresid  6627  fprlem1  8287  wfrlem5OLD  8315  dfoi  9508  frrlem15  9754  lubfval  18305  glbfval  18318  odulub  18362  oduglb  18364  dvlog  26166  dvlog2  26168  issubgr  28566  finsumvtxdg2size  28845  sitgclg  33410  fourierdlem57  44958  fourierdlem74  44975  fourierdlem75  44976
  Copyright terms: Public domain W3C validator