Theorem reseq2 5933

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 5639	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4156	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5637	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5637	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2800	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1547  Vcvv 3432   ∩ cin 3889   × cxp 5623   ↾ cres 5627

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 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-in 3897  df-opab 5142  df-xp 5631  df-res 5637

This theorem is referenced by:  reseq2i  5935  reseq2d  5938  resabs1  5965  resima2  5975  reldisjun  5991  imaeq2  6015  resdisj  6127  dfpo2  6254  fimadmfoALT  6757  fressnfv  7110  tfrlem1  8312  tfrlem9  8321  tfrlem11  8324  tfrlem12  8325  tfr2b  8332  tz7.44-1  8342  tz7.44-2  8343  tz7.44-3  8344  rdglem1  8351  fnfi  9109  fseqenlem1  9944  rtrclreclem4  15021  psgnprfval1  19495  gsumzaddlem  19894  gsum2dlem2  19944  gsumle  20118  znunithash  21546  islinds  21791  lmbr2  23249  lmff  23291  kgencn2  23547  ptcmpfi  23803  tsmsgsum  24129  tsmsres  24134  tsmsf1o  24135  tsmsxplem1  24143  tsmsxp  24145  ustval  24193  xrge0gsumle  24824  xrge0tsms  24825  lmmbr2  25251  lmcau  25305  limcun  25887  jensen  26977  wilthlem2  27057  wilthlem3  27058  hhssnvt  31361  hhsssh  31365  foresf1o  32599  xrge0tsmsd  33161  rprmdvdsprod  33624  esumsnf  34255  subfacp1lem3  35417  subfacp1lem5  35419  erdszelem1  35426  erdsze  35437  erdsze2lem2  35439  cvmscbv  35493  cvmshmeo  35506  cvmsss2  35509  eldm3  35996  dfrdg2  36028  bj-diagval  37541  mbfresfi  38040  disjresin  38617  elcoeleqvrels  39053  eleldisjs  39202  eldisjeq  39215  eqvrelqseqdisj3  39319  mzpcompact2lem  43207  seff  44760  wessf1ornlem  45639  fouriersw  46681  sge0tsms  46830  sge0f1o  46832  sge0sup  46841  meadjuni  46907  ismeannd  46917  psmeasurelem  46920  psmeasure  46921  omeunile  46955  isomennd  46981  hoidmvlelem3  47047