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

Theorem reseq12i 5888
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 5886 . 2 (𝐴𝐶) = (𝐵𝐶)
3 reseqi.2 . . 3 𝐶 = 𝐷
43reseq2i 5887 . 2 (𝐵𝐶) = (𝐵𝐷)
52, 4eqtri 2768 1 (𝐴𝐶) = (𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cres 5592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-in 3899  df-opab 5142  df-xp 5596  df-res 5602
This theorem is referenced by:  cnvresid  6511  fprlem1  8107  wfrlem5OLD  8135  dfoi  9248  frrlem15  9516  lubfval  18066  glbfval  18079  odulub  18123  oduglb  18125  dvlog  25804  dvlog2  25806  issubgr  27636  finsumvtxdg2size  27915  sitgclg  32305  fourierdlem57  43675  fourierdlem74  43692  fourierdlem75  43693
  Copyright terms: Public domain W3C validator