Theorem reseq2 5964

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 5664	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4117	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5662	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5662	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1569  Vcvv 3450   ∩ cin 4089   × cxp 5648   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4091  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  reseq2i  5966  reseq2d  5969  resabs1  5996  reldmun  6022  reldisjunOLD  6023  imaeq2  6047  resima2  6056  resdisj  6160  dfpo2  6299  fimadmfoALT  6808  fressnfv  7165  tfrlem1  8387  tfrlem9  8397  tfrlem11  8400  tfrlem12  8401  tfr2b  8408  tz7.44-1  8418  tz7.44-2  8419  tz7.44-3  8420  rdglem1  8427  fnfi  9197  fseqenlem1  10107  rtrclreclem4  15220  psgnprfval1  19742  gsumzaddlem  20141  gsum2dlem2  20191  gsumle  20365  znunithash  21876  islinds  22121  lmbr2  23583  lmff  23625  kgencn2  23882  ptcmpfi  24138  tsmsgsum  24464  tsmsres  24469  tsmsf1o  24470  tsmsxplem1  24478  tsmsxp  24480  ustval  24528  xrge0gsumle  25159  xrge0tsms  25160  lmmbr2  25586  lmcau  25640  limcun  26221  jensen  27322  wilthlem2  27402  wilthlem3  27403  hhssnvt  31873  hhsssh  31877  foresf1o  33148  xrge0tsmsd  33681  rprmdvdsprod  34113  esumsnf  34743  subfacp1lem3  36034  subfacp1lem5  36036  erdszelem1  36043  erdsze  36054  erdsze2lem2  36056  cvmscbv  36110  cvmshmeo  36123  cvmsss2  36126  eldm3  36619  dfrdg2  36650  bj-diagval  38189  mbfresfi  38678  disjresin  39269  elcoeleqvrels  39705  eleldisjs  39854  eldisjeq  39867  eqvrelqseqdisj3  39971  mzpcompact2lem  43856  seff  45387  wessf1ornlem  46294  fouriersw  47335  sge0tsms  47484  sge0f1o  47486  sge0sup  47495  meadjuni  47561  ismeannd  47571  psmeasurelem  47574  psmeasure  47575  omeunile  47609  isomennd  47635  hoidmvlelem3  47701