Theorem reseq12d 5977

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3909  df-opab 5172  df-xp 5665  df-res 5671

This theorem is used by:  f1ossf1o  7126  csbfrecsg  8287  tfrlem3a  8369  oieq1  9488  oieq2  9489  ackbij2lem3  10246  setsvalg  17264  resfval  17987  resfval2  17988  resf2nd  17990  lubfval  18442  glbfval  18455  dpjfval  20190  znval  21754  psrval  22136  prdsdsf  24599  prdsxmet  24601  imasdsf1olem  24605  xpsxmetlem  24611  xpsmet  24614  isxms  24679  isms  24681  setsxms  24711  setsms  24712  ressxms  24757  ressms  24758  prdsxmslem2  24761  cphsscph  25485  iscms  25579  cmsss  25585  cssbn  25609  minveclem3a  25661  dvmptresicc  26150  dvcmulf  26179  efcvx  26692  issubgr  29739  ispth  30193  clwlknf1oclwwlkn  30562  eucrct2eupth  30733  ressply1evls1  33983  isrrext  34518  prdsbnd2  38553  cnpwstotbnd  38555  ldualset  40006  itgcoscmulx  46805  fourierdlem73  47015  sge0fodjrnlem  47252  vonval  47376  tmachlem-agreeself  47772  tmachlem-agreeprod  47773  dfateq12d  48022  isisubgr  48786  rngchomrnghmresALTV  49202  fdivval  49477