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

Theorem reseq12d 5998
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 5996 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5997 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2777 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  cres 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-opab 5206  df-xp 5691  df-res 5697
This theorem is referenced by:  f1ossf1o  7148  csbfrecsg  8309  tfrlem3a  8417  oieq1  9552  oieq2  9553  ackbij2lem3  10280  setsvalg  17203  resfval  17937  resfval2  17938  resf2nd  17940  lubfval  18395  glbfval  18408  dpjfval  20075  znval  21550  psrval  21935  prdsdsf  24377  prdsxmet  24379  imasdsf1olem  24383  xpsxmetlem  24389  xpsmet  24392  isxms  24457  isms  24459  setsxms  24491  setsms  24492  ressxms  24538  ressms  24539  prdsxmslem2  24542  cphsscph  25285  iscms  25379  cmsss  25385  cssbn  25409  minveclem3a  25461  dvmptresicc  25951  dvcmulf  25982  efcvx  26493  issubgr  29288  ispth  29741  clwlknf1oclwwlkn  30103  eucrct2eupth  30264  padct  32731  isrrext  34001  prdsbnd2  37802  cnpwstotbnd  37804  ldualset  39126  itgcoscmulx  45984  fourierdlem73  46194  sge0fodjrnlem  46431  vonval  46555  dfateq12d  47138  isisubgr  47848  rngchomrnghmresALTV  48195  fdivval  48460
  Copyright terms: Public domain W3C validator