Theorem reseq12d 5552

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

Syntax hints:   → wi 4   = wceq 1632   ↾ cres 5268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-opab 4865  df-xp 5272  df-res 5278

This theorem is referenced by:  tfrlem3a  7643  oieq1  8584  oieq2  8585  ackbij2lem3  9275  setsvalg  16109  resfval  16773  resfval2  16774  resf2nd  16776  lubfval  17199  glbfval  17212  dpjfval  18674  psrval  19584  znval  20105  prdsdsf  22393  prdsxmet  22395  imasdsf1olem  22399  xpsxmetlem  22405  xpsmet  22408  isxms  22473  isms  22475  setsxms  22505  setsms  22506  ressxms  22551  ressms  22552  prdsxmslem2  22555  iscms  23362  cmsss  23367  minveclem3a  23418  dvcmulf  23927  efcvx  24422  issubgr  26383  ispth  26850  clwlknf1oclwwlkn  27249  eucrct2eupth  27418  padct  29827  isrrext  30374  csbwrecsg  33502  prdsbnd2  33925  cnpwstotbnd  33927  ldualset  34933  dvmptresicc  40655  itgcoscmulx  40706  fourierdlem73  40917  sge0fodjrnlem  41154  vonval  41278  dfateq12d  41733  rngchomrnghmresALTV  42524  fdivval  42861