Theorem reseq12d 5936

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 5934	. 2 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
3		reseqd.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	reseq2d 5935	. 2 ⊢ (𝜑 → (𝐵 ↾ 𝐶) = (𝐵 ↾ 𝐷))
5	2, 4	eqtrd 2768	1 ⊢ (𝜑 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐷))

Syntax hints:   → wi 4   = wceq 1541   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-in 3906  df-opab 5158  df-xp 5627  df-res 5633

This theorem is referenced by:  f1ossf1o  7070  csbfrecsg  8223  tfrlem3a  8305  oieq1  9408  oieq2  9409  ackbij2lem3  10141  setsvalg  17087  resfval  17809  resfval2  17810  resf2nd  17812  lubfval  18264  glbfval  18277  dpjfval  19979  znval  21482  psrval  21862  prdsdsf  24292  prdsxmet  24294  imasdsf1olem  24298  xpsxmetlem  24304  xpsmet  24307  isxms  24372  isms  24374  setsxms  24404  setsms  24405  ressxms  24450  ressms  24451  prdsxmslem2  24454  cphsscph  25188  iscms  25282  cmsss  25288  cssbn  25312  minveclem3a  25364  dvmptresicc  25854  dvcmulf  25885  efcvx  26396  issubgr  29260  ispth  29710  clwlknf1oclwwlkn  30075  eucrct2eupth  30236  padct  32712  ressply1evls1  33539  isrrext  34024  prdsbnd2  37845  cnpwstotbnd  37847  ldualset  39234  itgcoscmulx  46081  fourierdlem73  46291  sge0fodjrnlem  46528  vonval  46652  dfateq12d  47240  isisubgr  47976  rngchomrnghmresALTV  48393  fdivval  48654