Theorem reseq12d 5982

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

Step	Hyp	Ref	Expression
1		reseqd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	reseq1d 5980	. 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3		reseqd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	reseq2d 5981	. 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷))
5	2, 4	eqtrd 2798	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094  df-opab 5171  df-xp 5661  df-res 5667

This theorem is used by:  f1ossf1o  7153  csbfrecsg  8330  tfrlem3a  8412  oieq1  9533  oieq2  9534  ackbij2lem3  10345  setsvalg  17373  resfval  18096  resfval2  18097  resf2nd  18099  lubfval  18551  glbfval  18564  dpjfval  20301  znval  21871  psrval  22253  prdsdsf  24716  prdsxmet  24718  imasdsf1olem  24722  xpsxmetlem  24728  xpsmet  24731  isxms  24796  isms  24798  setsxms  24828  setsms  24829  ressxms  24874  ressms  24875  prdsxmslem2  24878  cphsscph  25602  iscms  25696  cmsss  25702  cssbn  25726  minveclem3a  25778  dvmptresicc  26266  dvcmulf  26295  efcvx  26806  issubgr  29882  ispth  30336  clwlknf1oclwwlkn  30705  eucrct2eupth  30876  ressply1evls1  34167  isrrext  34702  prdsbnd2  38921  cnpwstotbnd  38923  ldualset  40374  itgcoscmulx  47184  fourierdlem73  47394  sge0fodjrnlem  47631  vonval  47755  tmachlem-agreeself  48151  tmachlem-agreeprod  48152  dfateq12d  48401  isisubgr  49165  rngchomrnghmresALTV  49581  fdivval  49856