Theorem reseq2 5937

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 5652	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4177	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5650	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5650	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3446   ∩ cin 3912   × cxp 5636   ↾ cres 5640

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-in 3920  df-opab 5173  df-xp 5644  df-res 5650

This theorem is referenced by:  reseq2i  5939  reseq2d  5942  resabs1  5972  resima2  5977  imaeq2  6014  resdisj  6126  dfpo2  6253  fimadmfoALT  6772  fressnfv  7111  tfrlem1  8327  tfrlem9  8336  tfrlem11  8339  tfrlem12  8340  tfr2b  8347  tz7.44-1  8357  tz7.44-2  8358  tz7.44-3  8359  rdglem1  8366  fnfi  9132  fseqenlem1  9969  rtrclreclem4  14958  psgnprfval1  19318  gsumzaddlem  19712  gsum2dlem2  19762  znunithash  21008  islinds  21252  lmbr2  22647  lmff  22689  kgencn2  22945  ptcmpfi  23201  tsmsgsum  23527  tsmsres  23532  tsmsf1o  23533  tsmsxplem1  23541  tsmsxp  23543  ustval  23591  xrge0gsumle  24233  xrge0tsms  24234  lmmbr2  24660  lmcau  24714  limcun  25296  jensen  26375  wilthlem2  26455  wilthlem3  26456  hhssnvt  30270  hhsssh  30274  foresf1o  31495  reldisjun  31588  xrge0tsmsd  31969  gsumle  32002  esumsnf  32752  subfacp1lem3  33863  subfacp1lem5  33865  erdszelem1  33872  erdsze  33883  erdsze2lem2  33885  cvmscbv  33939  cvmshmeo  33952  cvmsss2  33955  eldm3  34420  dfrdg2  34456  bj-diagval  35718  mbfresfi  36197  disjresin  36770  elcoeleqvrels  37130  eleldisjs  37263  eldisjeq  37276  eqvrelqseqdisj3  37366  mzpcompact2lem  41132  seff  42711  wessf1ornlem  43525  fouriersw  44592  sge0tsms  44741  sge0f1o  44743  sge0sup  44752  meadjuni  44818  ismeannd  44828  psmeasurelem  44831  psmeasure  44832  omeunile  44866  isomennd  44892  hoidmvlelem3  44958