Theorem reseq2 5813

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 5533	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4139	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5531	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5531	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1538  Vcvv 3441   ∩ cin 3880   × cxp 5517   ↾ cres 5521

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888  df-opab 5093  df-xp 5525  df-res 5531

This theorem is referenced by:  reseq2i  5815  reseq2d  5818  resabs1  5848  resima2  5853  imaeq2  5892  resdisj  5993  fimadmfoALT  6576  fressnfv  6899  tfrlem1  7995  tfrlem9  8004  tfrlem11  8007  tfrlem12  8008  tfr2b  8015  tz7.44-1  8025  tz7.44-2  8026  tz7.44-3  8027  rdglem1  8034  fnfi  8780  fseqenlem1  9435  rtrclreclem4  14412  psgnprfval1  18642  gsumzaddlem  19034  gsum2dlem2  19084  znunithash  20256  islinds  20498  lmbr2  21864  lmff  21906  kgencn2  22162  ptcmpfi  22418  tsmsgsum  22744  tsmsres  22749  tsmsf1o  22750  tsmsxplem1  22758  tsmsxp  22760  ustval  22808  xrge0gsumle  23438  xrge0tsms  23439  lmmbr2  23863  lmcau  23917  limcun  24498  jensen  25574  wilthlem2  25654  wilthlem3  25655  hhssnvt  29048  hhsssh  29052  foresf1o  30273  reldisjun  30366  xrge0tsmsd  30742  gsumle  30775  esumsnf  31433  subfacp1lem3  32542  subfacp1lem5  32544  erdszelem1  32551  erdsze  32562  erdsze2lem2  32564  cvmscbv  32618  cvmshmeo  32631  cvmsss2  32634  dfpo2  33104  eldm3  33110  dfrdg2  33153  bj-diagval  34589  mbfresfi  35103  elcoeleqvrels  35990  eleldisjs  36121  eldisjeq  36134  mzpcompact2lem  39692  seff  41013  wessf1ornlem  41811  fouriersw  42873  sge0tsms  43019  sge0f1o  43021  sge0sup  43030  meadjuni  43096  ismeannd  43106  psmeasurelem  43109  psmeasure  43110  omeunile  43144  isomennd  43170  hoidmvlelem3  43236