Theorem reseq2 5965

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 5665	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4166	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5663	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5663	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3451   ∩ cin 3898   × cxp 5649   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3906  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  reseq2i  5967  reseq2d  5970  resabs1  5997  reldmun  6023  reldisjunOLD  6024  imaeq2  6048  resima2  6057  resdisj  6161  dfpo2  6298  fimadmfoALT  6805  fressnfv  7162  tfrlem1  8376  tfrlem9  8386  tfrlem11  8389  tfrlem12  8390  tfr2b  8397  tz7.44-1  8407  tz7.44-2  8408  tz7.44-3  8409  rdglem1  8416  fnfi  9186  fseqenlem1  10096  rtrclreclem4  15207  psgnprfval1  19729  gsumzaddlem  20128  gsum2dlem2  20178  gsumle  20352  znunithash  21863  islinds  22108  lmbr2  23570  lmff  23612  kgencn2  23869  ptcmpfi  24125  tsmsgsum  24451  tsmsres  24456  tsmsf1o  24457  tsmsxplem1  24465  tsmsxp  24467  ustval  24515  xrge0gsumle  25146  xrge0tsms  25147  lmmbr2  25573  lmcau  25627  limcun  26208  jensen  27309  wilthlem2  27389  wilthlem3  27390  hhssnvt  31860  hhsssh  31864  foresf1o  33093  xrge0tsmsd  33627  rprmdvdsprod  34059  esumsnf  34689  subfacp1lem3  35926  subfacp1lem5  35928  erdszelem1  35935  erdsze  35946  erdsze2lem2  35948  cvmscbv  36002  cvmshmeo  36015  cvmsss2  36018  eldm3  36505  dfrdg2  36537  bj-diagval  38075  mbfresfi  38564  disjresin  39155  elcoeleqvrels  39591  eleldisjs  39740  eldisjeq  39753  eqvrelqseqdisj3  39857  mzpcompact2lem  43741  seff  45278  wessf1ornlem  46169  fouriersw  47210  sge0tsms  47359  sge0f1o  47361  sge0sup  47370  meadjuni  47436  ismeannd  47446  psmeasurelem  47449  psmeasure  47450  omeunile  47484  isomennd  47510  hoidmvlelem3  47576