Theorem reseq2 5995

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

Syntax hints:   → wi 4   = wceq 1537  Vcvv 3478   ∩ cin 3962   × cxp 5687   ↾ cres 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-in 3970  df-opab 5211  df-xp 5695  df-res 5701

This theorem is referenced by:  reseq2i  5997  reseq2d  6000  resabs1  6027  resima2  6036  reldisjun  6052  imaeq2  6076  resdisj  6191  dfpo2  6318  fimadmfoALT  6832  fressnfv  7180  tfrlem1  8415  tfrlem9  8424  tfrlem11  8427  tfrlem12  8428  tfr2b  8435  tz7.44-1  8445  tz7.44-2  8446  tz7.44-3  8447  rdglem1  8454  fnfi  9216  fseqenlem1  10062  rtrclreclem4  15097  psgnprfval1  19555  gsumzaddlem  19954  gsum2dlem2  20004  znunithash  21601  islinds  21847  lmbr2  23283  lmff  23325  kgencn2  23581  ptcmpfi  23837  tsmsgsum  24163  tsmsres  24168  tsmsf1o  24169  tsmsxplem1  24177  tsmsxp  24179  ustval  24227  xrge0gsumle  24869  xrge0tsms  24870  lmmbr2  25307  lmcau  25361  limcun  25945  jensen  27047  wilthlem2  27127  wilthlem3  27128  hhssnvt  31294  hhsssh  31298  foresf1o  32532  xrge0tsmsd  33048  gsumle  33084  rprmdvdsprod  33542  esumsnf  34045  subfacp1lem3  35167  subfacp1lem5  35169  erdszelem1  35176  erdsze  35187  erdsze2lem2  35189  cvmscbv  35243  cvmshmeo  35256  cvmsss2  35259  eldm3  35741  dfrdg2  35777  bj-diagval  37157  mbfresfi  37653  disjresin  38221  elcoeleqvrels  38577  eleldisjs  38710  eldisjeq  38723  eqvrelqseqdisj3  38813  mzpcompact2lem  42739  seff  44305  wessf1ornlem  45128  fouriersw  46187  sge0tsms  46336  sge0f1o  46338  sge0sup  46347  meadjuni  46413  ismeannd  46423  psmeasurelem  46426  psmeasure  46427  omeunile  46461  isomennd  46487  hoidmvlelem3  46553