Theorem reseq2 5975

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 5677	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4174	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5675	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5675	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1570  Vcvv 3455   ∩ cin 3905   × cxp 5661   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3913  df-opab 5175  df-xp 5669  df-res 5675

This theorem is referenced by:  reseq2i  5977  reseq2d  5980  resabs1  6007  resima2  6017  reldmun  6035  reldisjunOLD  6036  imaeq2  6060  resdisj  6169  dfpo2  6299  fimadmfoALT  6805  fressnfv  7159  tfrlem1  8363  tfrlem9  8373  tfrlem11  8376  tfrlem12  8377  tfr2b  8384  tz7.44-1  8394  tz7.44-2  8395  tz7.44-3  8396  rdglem1  8403  fnfi  9163  fseqenlem1  10009  rtrclreclem4  15100  psgnprfval1  19593  gsumzaddlem  19992  gsum2dlem2  20042  gsumle  20216  znunithash  21695  islinds  21940  lmbr2  23397  lmff  23439  kgencn2  23695  ptcmpfi  23951  tsmsgsum  24277  tsmsres  24282  tsmsf1o  24283  tsmsxplem1  24291  tsmsxp  24293  ustval  24341  xrge0gsumle  24972  xrge0tsms  24973  lmmbr2  25399  lmcau  25453  limcun  26035  jensen  27134  wilthlem2  27214  wilthlem3  27215  hhssnvt  31598  hhsssh  31602  foresf1o  32831  xrge0tsmsd  33374  rprmdvdsprod  33805  esumsnf  34435  subfacp1lem3  35655  subfacp1lem5  35657  erdszelem1  35664  erdsze  35675  erdsze2lem2  35677  cvmscbv  35731  cvmshmeo  35744  cvmsss2  35747  eldm3  36234  dfrdg2  36266  bj-diagval  37799  mbfresfi  38298  disjresin  38873  elcoeleqvrels  39309  eleldisjs  39458  eldisjeq  39471  eqvrelqseqdisj3  39575  mzpcompact2lem  43465  seff  45002  wessf1ornlem  45886  fouriersw  46928  sge0tsms  47077  sge0f1o  47079  sge0sup  47088  meadjuni  47154  ismeannd  47164  psmeasurelem  47167  psmeasure  47168  omeunile  47202  isomennd  47228  hoidmvlelem3  47294