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

Theorem reseq12i 5998
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 5996 . 2 (𝐴𝐶) = (𝐵𝐶)
3 reseqi.2 . . 3 𝐶 = 𝐷
43reseq2i 5997 . 2 (𝐵𝐶) = (𝐵𝐷)
52, 4eqtri 2763 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  cres 5691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-in 3970  df-opab 5211  df-xp 5695  df-res 5701
This theorem is referenced by:  cnvresid  6647  fprlem1  8324  wfrlem5OLD  8352  dfoi  9549  frrlem15  9795  lubfval  18408  glbfval  18421  odulub  18465  oduglb  18467  dvlog  26708  dvlog2  26710  issubgr  29303  finsumvtxdg2size  29583  sitgclg  34324  fourierdlem57  46119  fourierdlem74  46136  fourierdlem75  46137
  Copyright terms: Public domain W3C validator