Theorem reseq12d 5566

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

Syntax hints:   → wi 4   = wceq 1652   ↾ cres 5279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3739  df-opab 4872  df-xp 5283  df-res 5289

This theorem is referenced by:  f1ossf1o  6586  tfrlem3a  7677  oieq1  8624  oieq2  8625  ackbij2lem3  9316  setsvalg  16162  resfval  16819  resfval2  16820  resf2nd  16822  lubfval  17246  glbfval  17259  dpjfval  18721  psrval  19636  znval  20156  prdsdsf  22451  prdsxmet  22453  imasdsf1olem  22457  xpsxmetlem  22463  xpsmet  22466  isxms  22531  isms  22533  setsxms  22563  setsms  22564  ressxms  22609  ressms  22610  prdsxmslem2  22613  iscms  23422  cmsss  23428  cssbn  23452  minveclem3a  23487  dvcmulf  23999  efcvx  24494  issubgr  26442  ispth  26910  clwlknf1oclwwlkn  27311  eucrct2eupth  27481  padct  29881  isrrext  30426  csbwrecsg  33539  prdsbnd2  33948  cnpwstotbnd  33950  ldualset  35013  dvmptresicc  40704  itgcoscmulx  40754  fourierdlem73  40965  sge0fodjrnlem  41202  vonval  41326  dfateq12d  41806  rngchomrnghmresALTV  42597  fdivval  42934