Theorem reseq12d 5954

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

Syntax hints:   → wi 4   = wceq 1540   ↾ cres 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924  df-opab 5173  df-xp 5647  df-res 5653

This theorem is referenced by:  f1ossf1o  7103  csbfrecsg  8266  tfrlem3a  8348  oieq1  9472  oieq2  9473  ackbij2lem3  10200  setsvalg  17143  resfval  17861  resfval2  17862  resf2nd  17864  lubfval  18316  glbfval  18329  dpjfval  19994  znval  21452  psrval  21831  prdsdsf  24262  prdsxmet  24264  imasdsf1olem  24268  xpsxmetlem  24274  xpsmet  24277  isxms  24342  isms  24344  setsxms  24374  setsms  24375  ressxms  24420  ressms  24421  prdsxmslem2  24424  cphsscph  25158  iscms  25252  cmsss  25258  cssbn  25282  minveclem3a  25334  dvmptresicc  25824  dvcmulf  25855  efcvx  26366  issubgr  29205  ispth  29658  clwlknf1oclwwlkn  30020  eucrct2eupth  30181  padct  32650  ressply1evls1  33541  isrrext  33997  prdsbnd2  37796  cnpwstotbnd  37798  ldualset  39125  itgcoscmulx  45974  fourierdlem73  46184  sge0fodjrnlem  46421  vonval  46545  dfateq12d  47131  isisubgr  47866  rngchomrnghmresALTV  48271  fdivval  48532