Theorem reseq12d 5998

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-opab 5206  df-xp 5691  df-res 5697

This theorem is referenced by:  f1ossf1o  7148  csbfrecsg  8309  tfrlem3a  8417  oieq1  9552  oieq2  9553  ackbij2lem3  10280  setsvalg  17203  resfval  17937  resfval2  17938  resf2nd  17940  lubfval  18395  glbfval  18408  dpjfval  20075  znval  21550  psrval  21935  prdsdsf  24377  prdsxmet  24379  imasdsf1olem  24383  xpsxmetlem  24389  xpsmet  24392  isxms  24457  isms  24459  setsxms  24491  setsms  24492  ressxms  24538  ressms  24539  prdsxmslem2  24542  cphsscph  25285  iscms  25379  cmsss  25385  cssbn  25409  minveclem3a  25461  dvmptresicc  25951  dvcmulf  25982  efcvx  26493  issubgr  29288  ispth  29741  clwlknf1oclwwlkn  30103  eucrct2eupth  30264  padct  32731  isrrext  34001  prdsbnd2  37802  cnpwstotbnd  37804  ldualset  39126  itgcoscmulx  45984  fourierdlem73  46194  sge0fodjrnlem  46431  vonval  46555  dfateq12d  47138  isisubgr  47848  rngchomrnghmresALTV  48195  fdivval  48460