Theorem reseq2 5814

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3397   ∩ cin 3840   × cxp 5517   ↾ cres 5521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-in 3848  df-opab 5090  df-xp 5525  df-res 5531

This theorem is referenced by:  reseq2i  5816  reseq2d  5819  resabs1  5849  resima2  5854  imaeq2  5893  resdisj  5995  fimadmfoALT  6597  fressnfv  6926  tfrlem1  8034  tfrlem9  8043  tfrlem11  8046  tfrlem12  8047  tfr2b  8054  tz7.44-1  8064  tz7.44-2  8065  tz7.44-3  8066  rdglem1  8073  fnfi  8771  fseqenlem1  9517  rtrclreclem4  14503  psgnprfval1  18761  gsumzaddlem  19153  gsum2dlem2  19203  znunithash  20376  islinds  20618  lmbr2  22003  lmff  22045  kgencn2  22301  ptcmpfi  22557  tsmsgsum  22883  tsmsres  22888  tsmsf1o  22889  tsmsxplem1  22897  tsmsxp  22899  ustval  22947  xrge0gsumle  23578  xrge0tsms  23579  lmmbr2  24004  lmcau  24058  limcun  24639  jensen  25718  wilthlem2  25798  wilthlem3  25799  hhssnvt  29192  hhsssh  29196  foresf1o  30416  reldisjun  30508  xrge0tsmsd  30886  gsumle  30919  esumsnf  31594  subfacp1lem3  32707  subfacp1lem5  32709  erdszelem1  32716  erdsze  32727  erdsze2lem2  32729  cvmscbv  32783  cvmshmeo  32796  cvmsss2  32799  dfpo2  33286  eldm3  33292  dfrdg2  33335  bj-diagval  34955  mbfresfi  35435  elcoeleqvrels  36320  eleldisjs  36451  eldisjeq  36464  mzpcompact2lem  40129  seff  41449  wessf1ornlem  42244  fouriersw  43298  sge0tsms  43444  sge0f1o  43446  sge0sup  43455  meadjuni  43521  ismeannd  43531  psmeasurelem  43534  psmeasure  43535  omeunile  43569  isomennd  43595  hoidmvlelem3  43661