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

Theorem reseq12d 5892
Description: Equality deduction for restrictions. (Contributed by NM, 21-Oct-2014.)
Hypotheses
Ref Expression
reseqd.1 (𝜑𝐴 = 𝐵)
reseqd.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
reseq12d (𝜑 → (𝐴𝐶) = (𝐵𝐷))

Proof of Theorem reseq12d
StepHypRef Expression
1 reseqd.1 . . 3 (𝜑𝐴 = 𝐵)
21reseq1d 5890 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5891 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2778 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  cres 5591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-in 3894  df-opab 5137  df-xp 5595  df-res 5601
This theorem is referenced by:  f1ossf1o  7000  csbfrecsg  8100  tfrlem3a  8208  oieq1  9271  oieq2  9272  ackbij2lem3  9997  setsvalg  16867  resfval  17607  resfval2  17608  resf2nd  17610  lubfval  18068  glbfval  18081  dpjfval  19658  znval  20739  psrval  21118  prdsdsf  23520  prdsxmet  23522  imasdsf1olem  23526  xpsxmetlem  23532  xpsmet  23535  isxms  23600  isms  23602  setsxms  23634  setsms  23635  ressxms  23681  ressms  23682  prdsxmslem2  23685  cphsscph  24415  iscms  24509  cmsss  24515  cssbn  24539  minveclem3a  24591  dvmptresicc  25080  dvcmulf  25109  efcvx  25608  issubgr  27638  ispth  28091  clwlknf1oclwwlkn  28448  eucrct2eupth  28609  padct  31054  isrrext  31950  prdsbnd2  35953  cnpwstotbnd  35955  ldualset  37139  itgcoscmulx  43510  fourierdlem73  43720  sge0fodjrnlem  43954  vonval  44078  dfateq12d  44618  rngchomrnghmresALTV  45554  fdivval  45885
  Copyright terms: Public domain W3C validator