Theorem reseq12d 5946

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

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-opab 5149  df-xp 5637  df-res 5643

This theorem is referenced by:  f1ossf1o  7082  csbfrecsg  8234  tfrlem3a  8316  oieq1  9427  oieq2  9428  ackbij2lem3  10162  setsvalg  17136  resfval  17859  resfval2  17860  resf2nd  17862  lubfval  18314  glbfval  18327  dpjfval  20032  znval  21515  psrval  21895  prdsdsf  24332  prdsxmet  24334  imasdsf1olem  24338  xpsxmetlem  24344  xpsmet  24347  isxms  24412  isms  24414  setsxms  24444  setsms  24445  ressxms  24490  ressms  24491  prdsxmslem2  24494  cphsscph  25218  iscms  25312  cmsss  25318  cssbn  25342  minveclem3a  25394  dvmptresicc  25883  dvcmulf  25912  efcvx  26414  issubgr  29340  ispth  29789  clwlknf1oclwwlkn  30154  eucrct2eupth  30315  ressply1evls1  33625  isrrext  34144  prdsbnd2  38116  cnpwstotbnd  38118  ldualset  39571  itgcoscmulx  46397  fourierdlem73  46607  sge0fodjrnlem  46844  vonval  46968  dfateq12d  47568  isisubgr  48332  rngchomrnghmresALTV  48749  fdivval  49009