Theorem reseq12d 5984

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-in 3915  df-opab 5179  df-xp 5672  df-res 5678

This theorem is used by:  f1ossf1o  7131  csbfrecsg  8290  tfrlem3a  8372  oieq1  9484  oieq2  9485  ackbij2lem3  10242  setsvalg  17251  resfval  17974  resfval2  17975  resf2nd  17977  lubfval  18429  glbfval  18442  dpjfval  20158  znval  21722  psrval  22102  prdsdsf  24561  prdsxmet  24563  imasdsf1olem  24567  xpsxmetlem  24573  xpsmet  24576  isxms  24641  isms  24643  setsxms  24673  setsms  24674  ressxms  24719  ressms  24720  prdsxmslem2  24723  cphsscph  25447  iscms  25541  cmsss  25547  cssbn  25571  minveclem3a  25623  dvmptresicc  26112  dvcmulf  26141  efcvx  26649  issubgr  29658  ispth  30107  clwlknf1oclwwlkn  30472  eucrct2eupth  30633  ressply1evls1  33886  isrrext  34421  prdsbnd2  38486  cnpwstotbnd  38488  ldualset  39939  itgcoscmulx  46723  fourierdlem73  46933  sge0fodjrnlem  47170  vonval  47294  dfateq12d  47903  isisubgr  48667  rngchomrnghmresALTV  49084  fdivval  49359