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

Theorem reseq12d 5318
 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 5316 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5317 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2644 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ↾ cres 5040 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-opab 4644  df-xp 5044  df-res 5050 This theorem is referenced by:  tfrlem3a  7360  oieq1  8300  oieq2  8301  ackbij2lem3  8946  setsvalg  15719  resfval  16375  resfval2  16376  resf2nd  16378  lubfval  16801  glbfval  16814  dpjfval  18277  psrval  19183  znval  19702  prdsdsf  21982  prdsxmet  21984  imasdsf1olem  21988  xpsxmetlem  21994  xpsmet  21997  isxms  22062  isms  22064  setsxms  22094  setsms  22095  ressxms  22140  ressms  22141  prdsxmslem2  22144  iscms  22950  cmsss  22955  minveclem3a  23006  dvcmulf  23514  efcvx  24007  ispth  26098  constr3pthlem1  26183  padct  28885  isrrext  29372  csbwrecsg  32349  prdsbnd2  32764  cnpwstotbnd  32766  ldualset  33430  dvmptresicc  38809  itgcoscmulx  38861  fourierdlem73  39072  sge0fodjrnlem  39309  vonval  39430  dfateq12d  39858  issubgr  40495  isPth  40929  eucrct2eupth  41413  rngchomrnghmresALTV  41788  fdivval  42131
 Copyright terms: Public domain W3C validator