Theorem reseq2 5934

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 5645	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4179	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5643	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5643	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3444   ∩ cin 3910   × cxp 5629   ↾ cres 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918  df-opab 5165  df-xp 5637  df-res 5643

This theorem is referenced by:  reseq2i  5936  reseq2d  5939  resabs1  5966  resima2  5976  reldisjun  5992  imaeq2  6016  resdisj  6130  dfpo2  6257  fimadmfoALT  6765  fressnfv  7114  tfrlem1  8321  tfrlem9  8330  tfrlem11  8333  tfrlem12  8334  tfr2b  8341  tz7.44-1  8351  tz7.44-2  8352  tz7.44-3  8353  rdglem1  8360  fnfi  9119  fseqenlem1  9953  rtrclreclem4  15003  psgnprfval1  19428  gsumzaddlem  19827  gsum2dlem2  19877  znunithash  21450  islinds  21694  lmbr2  23122  lmff  23164  kgencn2  23420  ptcmpfi  23676  tsmsgsum  24002  tsmsres  24007  tsmsf1o  24008  tsmsxplem1  24016  tsmsxp  24018  ustval  24066  xrge0gsumle  24698  xrge0tsms  24699  lmmbr2  25135  lmcau  25189  limcun  25772  jensen  26875  wilthlem2  26955  wilthlem3  26956  hhssnvt  31167  hhsssh  31171  foresf1o  32406  xrge0tsmsd  32975  gsumle  33011  rprmdvdsprod  33478  esumsnf  34027  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem1  35151  erdsze  35162  erdsze2lem2  35164  cvmscbv  35218  cvmshmeo  35231  cvmsss2  35234  eldm3  35721  dfrdg2  35756  bj-diagval  37135  mbfresfi  37633  disjresin  38201  elcoeleqvrels  38559  eleldisjs  38693  eldisjeq  38706  eqvrelqseqdisj3  38796  mzpcompact2lem  42712  seff  44271  wessf1ornlem  45152  fouriersw  46202  sge0tsms  46351  sge0f1o  46353  sge0sup  46362  meadjuni  46428  ismeannd  46438  psmeasurelem  46441  psmeasure  46442  omeunile  46476  isomennd  46502  hoidmvlelem3  46568