Theorem reseq2 5918

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 5625	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4165	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5623	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5623	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3436   ∩ cin 3896   × cxp 5609   ↾ cres 5613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904  df-opab 5149  df-xp 5617  df-res 5623

This theorem is referenced by:  reseq2i  5920  reseq2d  5923  resabs1  5950  resima2  5960  reldisjun  5976  imaeq2  6000  resdisj  6111  dfpo2  6238  fimadmfoALT  6741  fressnfv  7088  tfrlem1  8290  tfrlem9  8299  tfrlem11  8302  tfrlem12  8303  tfr2b  8310  tz7.44-1  8320  tz7.44-2  8321  tz7.44-3  8322  rdglem1  8329  fnfi  9082  fseqenlem1  9910  rtrclreclem4  14963  psgnprfval1  19429  gsumzaddlem  19828  gsum2dlem2  19878  gsumle  20052  znunithash  21496  islinds  21741  lmbr2  23169  lmff  23211  kgencn2  23467  ptcmpfi  23723  tsmsgsum  24049  tsmsres  24054  tsmsf1o  24055  tsmsxplem1  24063  tsmsxp  24065  ustval  24113  xrge0gsumle  24744  xrge0tsms  24745  lmmbr2  25181  lmcau  25235  limcun  25818  jensen  26921  wilthlem2  27001  wilthlem3  27002  hhssnvt  31237  hhsssh  31241  foresf1o  32476  xrge0tsmsd  33034  rprmdvdsprod  33491  esumsnf  34069  subfacp1lem3  35218  subfacp1lem5  35220  erdszelem1  35227  erdsze  35238  erdsze2lem2  35240  cvmscbv  35294  cvmshmeo  35307  cvmsss2  35310  eldm3  35797  dfrdg2  35829  bj-diagval  37208  mbfresfi  37706  disjresin  38274  elcoeleqvrels  38632  eleldisjs  38766  eldisjeq  38779  eqvrelqseqdisj3  38869  mzpcompact2lem  42784  seff  44342  wessf1ornlem  45222  fouriersw  46269  sge0tsms  46418  sge0f1o  46420  sge0sup  46429  meadjuni  46495  ismeannd  46505  psmeasurelem  46508  psmeasure  46509  omeunile  46543  isomennd  46569  hoidmvlelem3  46635