Theorem reseq2 5939

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3429   ∩ cin 3888   × cxp 5629   ↾ cres 5633

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896  df-opab 5148  df-xp 5637  df-res 5643

This theorem is referenced by:  reseq2i  5941  reseq2d  5944  resabs1  5971  resima2  5981  reldisjun  5997  imaeq2  6021  resdisj  6133  dfpo2  6260  fimadmfoALT  6763  fressnfv  7114  tfrlem1  8315  tfrlem9  8324  tfrlem11  8327  tfrlem12  8328  tfr2b  8335  tz7.44-1  8345  tz7.44-2  8346  tz7.44-3  8347  rdglem1  8354  fnfi  9112  fseqenlem1  9946  rtrclreclem4  15023  psgnprfval1  19497  gsumzaddlem  19896  gsum2dlem2  19946  gsumle  20120  znunithash  21544  islinds  21789  lmbr2  23224  lmff  23266  kgencn2  23522  ptcmpfi  23778  tsmsgsum  24104  tsmsres  24109  tsmsf1o  24110  tsmsxplem1  24118  tsmsxp  24120  ustval  24168  xrge0gsumle  24799  xrge0tsms  24800  lmmbr2  25226  lmcau  25280  limcun  25862  jensen  26952  wilthlem2  27032  wilthlem3  27033  hhssnvt  31336  hhsssh  31340  foresf1o  32574  xrge0tsmsd  33134  rprmdvdsprod  33594  esumsnf  34208  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem1  35373  erdsze  35384  erdsze2lem2  35386  cvmscbv  35440  cvmshmeo  35453  cvmsss2  35456  eldm3  35943  dfrdg2  35975  bj-diagval  37488  mbfresfi  37987  disjresin  38564  elcoeleqvrels  39000  eleldisjs  39149  eldisjeq  39162  eqvrelqseqdisj3  39266  mzpcompact2lem  43183  seff  44736  wessf1ornlem  45615  fouriersw  46659  sge0tsms  46808  sge0f1o  46810  sge0sup  46819  meadjuni  46885  ismeannd  46895  psmeasurelem  46898  psmeasure  46899  omeunile  46933  isomennd  46959  hoidmvlelem3  47025