Theorem reseq2 5956

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

Syntax hints:   → wi 4   = wceq 1559  Vcvv 3453   ∩ cin 3901   × cxp 5641   ↾ cres 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-in 3909  df-opab 5160  df-xp 5649  df-res 5655

This theorem is referenced by:  reseq2i  5958  reseq2d  5961  resabs1  5988  resima2  5998  reldmun  6016  reldisjunOLD  6017  imaeq2  6041  resdisj  6150  dfpo2  6278  fimadmfoALT  6784  fressnfv  7138  tfrlem1  8340  tfrlem9  8350  tfrlem11  8353  tfrlem12  8354  tfr2b  8361  tz7.44-1  8371  tz7.44-2  8372  tz7.44-3  8373  rdglem1  8380  fnfi  9140  fseqenlem1  9974  rtrclreclem4  15068  psgnprfval1  19553  gsumzaddlem  19952  gsum2dlem2  20002  gsumle  20176  znunithash  21604  islinds  21849  lmbr2  23307  lmff  23349  kgencn2  23605  ptcmpfi  23861  tsmsgsum  24187  tsmsres  24192  tsmsf1o  24193  tsmsxplem1  24201  tsmsxp  24203  ustval  24251  xrge0gsumle  24882  xrge0tsms  24883  lmmbr2  25309  lmcau  25363  limcun  25945  jensen  27041  wilthlem2  27121  wilthlem3  27122  hhssnvt  31425  hhsssh  31429  foresf1o  32663  xrge0tsmsd  33214  rprmdvdsprod  33691  esumsnf  34322  subfacp1lem3  35493  subfacp1lem5  35495  erdszelem1  35502  erdsze  35513  erdsze2lem2  35515  cvmscbv  35569  cvmshmeo  35582  cvmsss2  35585  eldm3  36072  dfrdg2  36104  bj-diagval  37627  mbfresfi  38126  disjresin  38703  elcoeleqvrels  39139  eleldisjs  39288  eldisjeq  39301  eqvrelqseqdisj3  39405  mzpcompact2lem  43293  seff  44846  wessf1ornlem  45724  fouriersw  46766  sge0tsms  46915  sge0f1o  46917  sge0sup  46926  meadjuni  46992  ismeannd  47002  psmeasurelem  47005  psmeasure  47006  omeunile  47040  isomennd  47066  hoidmvlelem3  47132