Theorem reseq12d 5937

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

Syntax hints:   → wi 4   = wceq 1542   ↾ cres 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-opab 5149  df-xp 5628  df-res 5634

This theorem is referenced by:  f1ossf1o  7073  csbfrecsg  8225  tfrlem3a  8307  oieq1  9418  oieq2  9419  ackbij2lem3  10151  setsvalg  17125  resfval  17848  resfval2  17849  resf2nd  17851  lubfval  18303  glbfval  18316  dpjfval  20021  znval  21523  psrval  21903  prdsdsf  24341  prdsxmet  24343  imasdsf1olem  24347  xpsxmetlem  24353  xpsmet  24356  isxms  24421  isms  24423  setsxms  24453  setsms  24454  ressxms  24499  ressms  24500  prdsxmslem2  24503  cphsscph  25227  iscms  25321  cmsss  25327  cssbn  25351  minveclem3a  25403  dvmptresicc  25892  dvcmulf  25921  efcvx  26430  issubgr  29359  ispth  29809  clwlknf1oclwwlkn  30174  eucrct2eupth  30335  ressply1evls1  33645  isrrext  34165  prdsbnd2  38127  cnpwstotbnd  38129  ldualset  39582  itgcoscmulx  46412  fourierdlem73  46622  sge0fodjrnlem  46859  vonval  46983  dfateq12d  47571  isisubgr  48335  rngchomrnghmresALTV  48752  fdivval  49012