Theorem reseq12d 5971

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  f1ossf1o  7121  csbfrecsg  8286  tfrlem3a  8368  oieq1  9490  oieq2  9491  ackbij2lem3  10299  setsvalg  17324  resfval  18047  resfval2  18048  resf2nd  18050  lubfval  18502  glbfval  18515  dpjfval  20251  znval  21821  psrval  22203  prdsdsf  24666  prdsxmet  24668  imasdsf1olem  24672  xpsxmetlem  24678  xpsmet  24681  isxms  24746  isms  24748  setsxms  24778  setsms  24779  ressxms  24824  ressms  24825  prdsxmslem2  24828  cphsscph  25552  iscms  25646  cmsss  25652  cssbn  25676  minveclem3a  25728  dvmptresicc  26216  dvcmulf  26245  efcvx  26758  issubgr  29834  ispth  30288  clwlknf1oclwwlkn  30657  eucrct2eupth  30828  ressply1evls1  34079  isrrext  34614  prdsbnd2  38697  cnpwstotbnd  38699  ldualset  40150  itgcoscmulx  46923  fourierdlem73  47133  sge0fodjrnlem  47370  vonval  47494  tmachlem-agreeself  47890  tmachlem-agreeprod  47891  dfateq12d  48140  isisubgr  48904  rngchomrnghmresALTV  49320  fdivval  49595