Theorem reseq2 5976

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 5690	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4212	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5688	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5688	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3474   ∩ cin 3947   × cxp 5674   ↾ cres 5678

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955  df-opab 5211  df-xp 5682  df-res 5688

This theorem is referenced by:  reseq2i  5978  reseq2d  5981  resabs1  6011  resima2  6016  reldisjun  6032  imaeq2  6055  resdisj  6168  dfpo2  6295  fimadmfoALT  6816  fressnfv  7160  tfrlem1  8378  tfrlem9  8387  tfrlem11  8390  tfrlem12  8391  tfr2b  8398  tz7.44-1  8408  tz7.44-2  8409  tz7.44-3  8410  rdglem1  8417  fnfi  9183  fseqenlem1  10021  rtrclreclem4  15012  psgnprfval1  19431  gsumzaddlem  19830  gsum2dlem2  19880  znunithash  21339  islinds  21583  lmbr2  22983  lmff  23025  kgencn2  23281  ptcmpfi  23537  tsmsgsum  23863  tsmsres  23868  tsmsf1o  23869  tsmsxplem1  23877  tsmsxp  23879  ustval  23927  xrge0gsumle  24569  xrge0tsms  24570  lmmbr2  25000  lmcau  25054  limcun  25636  jensen  26717  wilthlem2  26797  wilthlem3  26798  hhssnvt  30773  hhsssh  30777  foresf1o  31997  xrge0tsmsd  32467  gsumle  32500  esumsnf  33348  subfacp1lem3  34459  subfacp1lem5  34461  erdszelem1  34468  erdsze  34479  erdsze2lem2  34481  cvmscbv  34535  cvmshmeo  34548  cvmsss2  34551  eldm3  35023  dfrdg2  35059  bj-diagval  36358  mbfresfi  36837  disjresin  37409  elcoeleqvrels  37768  eleldisjs  37901  eldisjeq  37914  eqvrelqseqdisj3  38004  mzpcompact2lem  41791  seff  43370  wessf1ornlem  44183  fouriersw  45246  sge0tsms  45395  sge0f1o  45397  sge0sup  45406  meadjuni  45472  ismeannd  45482  psmeasurelem  45485  psmeasure  45486  omeunile  45520  isomennd  45546  hoidmvlelem3  45612