Theorem reseq2 5967

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 3906  df-opab 5168  df-xp 5661  df-res 5667

This theorem is used by:  reseq2i  5969  reseq2d  5972  resabs1  5999  resima2  6009  reldmun  6027  reldisjunOLD  6028  imaeq2  6052  resdisj  6162  dfpo2  6294  fimadmfoALT  6800  fressnfv  7157  tfrlem1  8364  tfrlem9  8374  tfrlem11  8377  tfrlem12  8378  tfr2b  8385  tz7.44-1  8395  tz7.44-2  8396  tz7.44-3  8397  rdglem1  8404  fnfi  9172  fseqenlem1  10027  rtrclreclem4  15134  psgnprfval1  19649  gsumzaddlem  20048  gsum2dlem2  20098  gsumle  20272  znunithash  21777  islinds  22022  lmbr2  23484  lmff  23526  kgencn2  23783  ptcmpfi  24039  tsmsgsum  24365  tsmsres  24370  tsmsf1o  24371  tsmsxplem1  24379  tsmsxp  24381  ustval  24429  xrge0gsumle  25060  xrge0tsms  25061  lmmbr2  25487  lmcau  25541  limcun  26122  jensen  27225  wilthlem2  27305  wilthlem3  27306  hhssnvt  31746  hhsssh  31750  foresf1o  32979  xrge0tsmsd  33513  rprmdvdsprod  33944  esumsnf  34574  subfacp1lem3  35761  subfacp1lem5  35763  erdszelem1  35770  erdsze  35781  erdsze2lem2  35783  cvmscbv  35837  cvmshmeo  35850  cvmsss2  35853  eldm3  36340  dfrdg2  36372  bj-diagval  37926  mbfresfi  38415  disjresin  38991  elcoeleqvrels  39427  eleldisjs  39576  eldisjeq  39589  eqvrelqseqdisj3  39693  mzpcompact2lem  43596  seff  45133  wessf1ornlem  46017  fouriersw  47059  sge0tsms  47208  sge0f1o  47210  sge0sup  47219  meadjuni  47285  ismeannd  47295  psmeasurelem  47298  psmeasure  47299  omeunile  47333  isomennd  47359  hoidmvlelem3  47425