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 2801	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915  df-opab 5177  df-xp 5670  df-res 5676

This theorem is used by:  f1ossf1o  7128  csbfrecsg  8283  tfrlem3a  8365  oieq1  9476  oieq2  9477  ackbij2lem3  10234  setsvalg  17236  resfval  17959  resfval2  17960  resf2nd  17962  lubfval  18414  glbfval  18427  dpjfval  20137  znval  21700  psrval  22080  prdsdsf  24539  prdsxmet  24541  imasdsf1olem  24545  xpsxmetlem  24551  xpsmet  24554  isxms  24619  isms  24621  setsxms  24651  setsms  24652  ressxms  24697  ressms  24698  prdsxmslem2  24701  cphsscph  25425  iscms  25519  cmsss  25525  cssbn  25549  minveclem3a  25601  dvmptresicc  26090  dvcmulf  26119  efcvx  26627  issubgr  29636  ispth  30085  clwlknf1oclwwlkn  30450  eucrct2eupth  30611  ressply1evls1  33868  isrrext  34403  prdsbnd2  38478  cnpwstotbnd  38480  ldualset  39931  itgcoscmulx  46715  fourierdlem73  46925  sge0fodjrnlem  47162  vonval  47286  dfateq12d  47895  isisubgr  48659  rngchomrnghmresALTV  49076  fdivval  49351