Theorem reseq2 5961

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 5668	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4195	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5666	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5666	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3459   ∩ cin 3925   × cxp 5652   ↾ cres 5656

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-in 3933  df-opab 5182  df-xp 5660  df-res 5666

This theorem is referenced by:  reseq2i  5963  reseq2d  5966  resabs1  5993  resima2  6003  reldisjun  6019  imaeq2  6043  resdisj  6158  dfpo2  6285  fimadmfoALT  6801  fressnfv  7150  tfrlem1  8390  tfrlem9  8399  tfrlem11  8402  tfrlem12  8403  tfr2b  8410  tz7.44-1  8420  tz7.44-2  8421  tz7.44-3  8422  rdglem1  8429  fnfi  9192  fseqenlem1  10038  rtrclreclem4  15080  psgnprfval1  19503  gsumzaddlem  19902  gsum2dlem2  19952  znunithash  21525  islinds  21769  lmbr2  23197  lmff  23239  kgencn2  23495  ptcmpfi  23751  tsmsgsum  24077  tsmsres  24082  tsmsf1o  24083  tsmsxplem1  24091  tsmsxp  24093  ustval  24141  xrge0gsumle  24773  xrge0tsms  24774  lmmbr2  25211  lmcau  25265  limcun  25848  jensen  26951  wilthlem2  27031  wilthlem3  27032  hhssnvt  31246  hhsssh  31250  foresf1o  32485  xrge0tsmsd  33056  gsumle  33092  rprmdvdsprod  33549  esumsnf  34095  subfacp1lem3  35204  subfacp1lem5  35206  erdszelem1  35213  erdsze  35224  erdsze2lem2  35226  cvmscbv  35280  cvmshmeo  35293  cvmsss2  35296  eldm3  35778  dfrdg2  35813  bj-diagval  37192  mbfresfi  37690  disjresin  38258  elcoeleqvrels  38613  eleldisjs  38746  eldisjeq  38759  eqvrelqseqdisj3  38849  mzpcompact2lem  42774  seff  44333  wessf1ornlem  45209  fouriersw  46260  sge0tsms  46409  sge0f1o  46411  sge0sup  46420  meadjuni  46486  ismeannd  46496  psmeasurelem  46499  psmeasure  46500  omeunile  46534  isomennd  46560  hoidmvlelem3  46626