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

Theorem reseq12d 5740
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 5738 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 reseqd.2 . . 3 (𝜑𝐶 = 𝐷)
43reseq2d 5739 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2831 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1522  cres 5450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-in 3870  df-opab 5029  df-xp 5454  df-res 5460
This theorem is referenced by:  f1ossf1o  6758  tfrlem3a  7870  oieq1  8827  oieq2  8828  ackbij2lem3  9514  setsvalg  16346  resfval  16996  resfval2  16997  resf2nd  16999  lubfval  17422  glbfval  17435  dpjfval  18899  psrval  19835  znval  20369  prdsdsf  22665  prdsxmet  22667  imasdsf1olem  22671  xpsxmetlem  22677  xpsmet  22680  isxms  22745  isms  22747  setsxms  22777  setsms  22778  ressxms  22823  ressms  22824  prdsxmslem2  22827  cphsscph  23542  iscms  23636  cmsss  23642  cssbn  23666  minveclem3a  23718  dvcmulf  24230  efcvx  24725  issubgr  26741  ispth  27196  clwlknf1oclwwlkn  27555  eucrct2eupthOLD  27718  eucrct2eupth  27719  padct  30148  isrrext  30863  csbwrecsg  34164  prdsbnd2  34630  cnpwstotbnd  34632  ldualset  35817  dvmptresicc  41771  itgcoscmulx  41821  fourierdlem73  42032  sge0fodjrnlem  42266  vonval  42390  dfateq12d  42867  rngchomrnghmresALTV  43771  fdivval  44106
  Copyright terms: Public domain W3C validator