Theorem reseq12d 5939

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

Syntax hints:   → wi 4   = wceq 1547   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-opab 5142  df-xp 5631  df-res 5637

This theorem is referenced by:  f1ossf1o  7077  csbfrecsg  8231  tfrlem3a  8313  oieq1  9424  oieq2  9425  ackbij2lem3  10160  setsvalg  17134  resfval  17857  resfval2  17858  resf2nd  17860  lubfval  18312  glbfval  18325  dpjfval  20030  znval  21517  psrval  21897  prdsdsf  24357  prdsxmet  24359  imasdsf1olem  24363  xpsxmetlem  24369  xpsmet  24372  isxms  24437  isms  24439  setsxms  24469  setsms  24470  ressxms  24515  ressms  24516  prdsxmslem2  24519  cphsscph  25243  iscms  25337  cmsss  25343  cssbn  25367  minveclem3a  25419  dvmptresicc  25908  dvcmulf  25937  efcvx  26439  issubgr  29365  ispth  29814  clwlknf1oclwwlkn  30179  eucrct2eupth  30340  ressply1evls1  33655  isrrext  34191  prdsbnd2  38169  cnpwstotbnd  38171  ldualset  39624  itgcoscmulx  46419  fourierdlem73  46629  sge0fodjrnlem  46866  vonval  46990  dfateq12d  47596  isisubgr  48360  rngchomrnghmresALTV  48777  fdivval  49037