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 5638	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4161	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5636	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5636	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3430   ∩ cin 3889   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-in 3897  df-opab 5149  df-xp 5630  df-res 5636

This theorem is referenced by:  reseq2i  5935  reseq2d  5938  resabs1  5965  resima2  5975  reldisjun  5991  imaeq2  6015  resdisj  6127  dfpo2  6254  fimadmfoALT  6757  fressnfv  7107  tfrlem1  8308  tfrlem9  8317  tfrlem11  8320  tfrlem12  8321  tfr2b  8328  tz7.44-1  8338  tz7.44-2  8339  tz7.44-3  8340  rdglem1  8347  fnfi  9105  fseqenlem1  9937  rtrclreclem4  15014  psgnprfval1  19488  gsumzaddlem  19887  gsum2dlem2  19937  gsumle  20111  znunithash  21554  islinds  21799  lmbr2  23234  lmff  23276  kgencn2  23532  ptcmpfi  23788  tsmsgsum  24114  tsmsres  24119  tsmsf1o  24120  tsmsxplem1  24128  tsmsxp  24130  ustval  24178  xrge0gsumle  24809  xrge0tsms  24810  lmmbr2  25236  lmcau  25290  limcun  25872  jensen  26966  wilthlem2  27046  wilthlem3  27047  hhssnvt  31351  hhsssh  31355  foresf1o  32589  xrge0tsmsd  33149  rprmdvdsprod  33609  esumsnf  34224  subfacp1lem3  35380  subfacp1lem5  35382  erdszelem1  35389  erdsze  35400  erdsze2lem2  35402  cvmscbv  35456  cvmshmeo  35469  cvmsss2  35472  eldm3  35959  dfrdg2  35991  bj-diagval  37504  mbfresfi  38001  disjresin  38578  elcoeleqvrels  39014  eleldisjs  39163  eldisjeq  39176  eqvrelqseqdisj3  39280  mzpcompact2lem  43197  seff  44754  wessf1ornlem  45633  fouriersw  46677  sge0tsms  46826  sge0f1o  46828  sge0sup  46837  meadjuni  46903  ismeannd  46913  psmeasurelem  46916  psmeasure  46917  omeunile  46951  isomennd  46977  hoidmvlelem3  47043