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

Theorem reseq12d 5819
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 5817 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5818 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2833 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cres 5521
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888  df-opab 5093  df-xp 5525  df-res 5531
This theorem is referenced by:  f1ossf1o  6867  tfrlem3a  7996  oieq1  8960  oieq2  8961  ackbij2lem3  9652  setsvalg  16504  resfval  17154  resfval2  17155  resf2nd  17157  lubfval  17580  glbfval  17593  dpjfval  19170  znval  20227  psrval  20600  prdsdsf  22974  prdsxmet  22976  imasdsf1olem  22980  xpsxmetlem  22986  xpsmet  22989  isxms  23054  isms  23056  setsxms  23086  setsms  23087  ressxms  23132  ressms  23133  prdsxmslem2  23136  cphsscph  23855  iscms  23949  cmsss  23955  cssbn  23979  minveclem3a  24031  dvmptresicc  24519  dvcmulf  24548  efcvx  25044  issubgr  27061  ispth  27512  clwlknf1oclwwlkn  27869  eucrct2eupth  28030  padct  30481  isrrext  31351  csbwrecsg  34741  prdsbnd2  35230  cnpwstotbnd  35232  ldualset  36418  itgcoscmulx  42606  fourierdlem73  42816  sge0fodjrnlem  43050  vonval  43174  dfateq12d  43677  rngchomrnghmresALTV  44615  fdivval  44948
  Copyright terms: Public domain W3C validator