Theorem reseq12d 5970

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  f1ossf1o  7129  csbfrecsg  8305  tfrlem3a  8387  oieq1  9509  oieq2  9510  ackbij2lem3  10321  setsvalg  17349  resfval  18072  resfval2  18073  resf2nd  18075  lubfval  18527  glbfval  18540  dpjfval  20276  znval  21846  psrval  22228  prdsdsf  24691  prdsxmet  24693  imasdsf1olem  24697  xpsxmetlem  24703  xpsmet  24706  isxms  24771  isms  24773  setsxms  24803  setsms  24804  ressxms  24849  ressms  24850  prdsxmslem2  24853  cphsscph  25577  iscms  25671  cmsss  25677  cssbn  25701  minveclem3a  25753  dvmptresicc  26241  dvcmulf  26270  efcvx  26781  issubgr  29857  ispth  30311  clwlknf1oclwwlkn  30680  eucrct2eupth  30851  ressply1evls1  34143  isrrext  34678  prdsbnd2  38822  cnpwstotbnd  38824  ldualset  40275  itgcoscmulx  47072  fourierdlem73  47282  sge0fodjrnlem  47519  vonval  47643  tmachlem-agreeself  48039  tmachlem-agreeprod  48040  dfateq12d  48289  isisubgr  49053  rngchomrnghmresALTV  49469  fdivval  49744