Theorem reseq12d 5397

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

Syntax hints:   → wi 4   = wceq 1483   ↾ cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-opab 4713  df-xp 5120  df-res 5126

This theorem is referenced by:  tfrlem3a  7473  oieq1  8417  oieq2  8418  ackbij2lem3  9063  setsvalg  15887  resfval  16552  resfval2  16553  resf2nd  16555  lubfval  16978  glbfval  16991  dpjfval  18454  psrval  19362  znval  19883  prdsdsf  22172  prdsxmet  22174  imasdsf1olem  22178  xpsxmetlem  22184  xpsmet  22187  isxms  22252  isms  22254  setsxms  22284  setsms  22285  ressxms  22330  ressms  22331  prdsxmslem2  22334  iscms  23142  cmsss  23147  minveclem3a  23198  dvcmulf  23708  efcvx  24203  issubgr  26163  ispth  26619  eucrct2eupth  27105  padct  29497  isrrext  30044  csbwrecsg  33173  prdsbnd2  33594  cnpwstotbnd  33596  ldualset  34412  dvmptresicc  40134  itgcoscmulx  40185  fourierdlem73  40396  sge0fodjrnlem  40633  vonval  40754  dfateq12d  41209  rngchomrnghmresALTV  41996  fdivval  42333