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

Theorem reseq12d 5357
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 5355 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5356 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2655 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  cres 5076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562  df-opab 4674  df-xp 5080  df-res 5086
This theorem is referenced by:  tfrlem3a  7418  oieq1  8361  oieq2  8362  ackbij2lem3  9007  setsvalg  15808  resfval  16473  resfval2  16474  resf2nd  16476  lubfval  16899  glbfval  16912  dpjfval  18375  psrval  19281  znval  19802  prdsdsf  22082  prdsxmet  22084  imasdsf1olem  22088  xpsxmetlem  22094  xpsmet  22097  isxms  22162  isms  22164  setsxms  22194  setsms  22195  ressxms  22240  ressms  22241  prdsxmslem2  22244  iscms  23050  cmsss  23055  minveclem3a  23106  dvcmulf  23614  efcvx  24107  issubgr  26056  ispth  26488  eucrct2eupth  26971  padct  29337  isrrext  29823  csbwrecsg  32802  prdsbnd2  33223  cnpwstotbnd  33225  ldualset  33889  dvmptresicc  39437  itgcoscmulx  39489  fourierdlem73  39700  sge0fodjrnlem  39937  vonval  40058  dfateq12d  40510  rngchomrnghmresALTV  41281  fdivval  41622
  Copyright terms: Public domain W3C validator