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

Theorem reseq12d 5544
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 5542 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5543 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2786 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1624  cres 5260
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-in 3714  df-opab 4857  df-xp 5264  df-res 5270
This theorem is referenced by:  tfrlem3a  7634  oieq1  8574  oieq2  8575  ackbij2lem3  9247  setsvalg  16081  resfval  16745  resfval2  16746  resf2nd  16748  lubfval  17171  glbfval  17184  dpjfval  18646  psrval  19556  znval  20077  prdsdsf  22365  prdsxmet  22367  imasdsf1olem  22371  xpsxmetlem  22377  xpsmet  22380  isxms  22445  isms  22447  setsxms  22477  setsms  22478  ressxms  22523  ressms  22524  prdsxmslem2  22527  iscms  23334  cmsss  23339  minveclem3a  23390  dvcmulf  23899  efcvx  24394  issubgr  26354  ispth  26821  clwlknf1oclwwlkn  27220  eucrct2eupth  27389  padct  29798  isrrext  30345  csbwrecsg  33476  prdsbnd2  33899  cnpwstotbnd  33901  ldualset  34907  dvmptresicc  40629  itgcoscmulx  40680  fourierdlem73  40891  sge0fodjrnlem  41128  vonval  41252  dfateq12d  41707  rngchomrnghmresALTV  42498  fdivval  42835
  Copyright terms: Public domain W3C validator