Theorem reseq2 5930

Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)

Assertion

Ref	Expression
reseq2	⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Proof of Theorem reseq2

Step	Hyp	Ref	Expression
1		xpeq1 5635	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4169	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5633	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5633	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3437   ∩ cin 3897   × cxp 5619   ↾ cres 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905  df-opab 5158  df-xp 5627  df-res 5633

This theorem is referenced by:  reseq2i  5932  reseq2d  5935  resabs1  5962  resima2  5972  reldisjun  5988  imaeq2  6012  resdisj  6124  dfpo2  6251  fimadmfoALT  6754  fressnfv  7102  tfrlem1  8304  tfrlem9  8313  tfrlem11  8316  tfrlem12  8317  tfr2b  8324  tz7.44-1  8334  tz7.44-2  8335  tz7.44-3  8336  rdglem1  8343  fnfi  9098  fseqenlem1  9926  rtrclreclem4  14975  psgnprfval1  19442  gsumzaddlem  19841  gsum2dlem2  19891  gsumle  20065  znunithash  21510  islinds  21755  lmbr2  23194  lmff  23236  kgencn2  23492  ptcmpfi  23748  tsmsgsum  24074  tsmsres  24079  tsmsf1o  24080  tsmsxplem1  24088  tsmsxp  24090  ustval  24138  xrge0gsumle  24769  xrge0tsms  24770  lmmbr2  25206  lmcau  25260  limcun  25843  jensen  26946  wilthlem2  27026  wilthlem3  27027  hhssnvt  31266  hhsssh  31270  foresf1o  32505  xrge0tsmsd  33083  rprmdvdsprod  33543  esumsnf  34149  subfacp1lem3  35298  subfacp1lem5  35300  erdszelem1  35307  erdsze  35318  erdsze2lem2  35320  cvmscbv  35374  cvmshmeo  35387  cvmsss2  35390  eldm3  35877  dfrdg2  35909  bj-diagval  37291  mbfresfi  37779  disjresin  38351  elcoeleqvrels  38764  eleldisjs  38899  eldisjeq  38912  eqvrelqseqdisj3  39002  mzpcompact2lem  42908  seff  44466  wessf1ornlem  45345  fouriersw  46391  sge0tsms  46540  sge0f1o  46542  sge0sup  46551  meadjuni  46617  ismeannd  46627  psmeasurelem  46630  psmeasure  46631  omeunile  46665  isomennd  46691  hoidmvlelem3  46757