Theorem reseq2 5975

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 5690	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4212	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5688	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5688	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3475   ∩ cin 3947   × cxp 5674   ↾ cres 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-in 3955  df-opab 5211  df-xp 5682  df-res 5688

This theorem is referenced by:  reseq2i  5977  reseq2d  5980  resabs1  6010  resima2  6015  reldisjun  6031  imaeq2  6054  resdisj  6166  dfpo2  6293  fimadmfoALT  6814  fressnfv  7155  tfrlem1  8373  tfrlem9  8382  tfrlem11  8385  tfrlem12  8386  tfr2b  8393  tz7.44-1  8403  tz7.44-2  8404  tz7.44-3  8405  rdglem1  8412  fnfi  9178  fseqenlem1  10016  rtrclreclem4  15005  psgnprfval1  19385  gsumzaddlem  19784  gsum2dlem2  19834  znunithash  21112  islinds  21356  lmbr2  22755  lmff  22797  kgencn2  23053  ptcmpfi  23309  tsmsgsum  23635  tsmsres  23640  tsmsf1o  23641  tsmsxplem1  23649  tsmsxp  23651  ustval  23699  xrge0gsumle  24341  xrge0tsms  24342  lmmbr2  24768  lmcau  24822  limcun  25404  jensen  26483  wilthlem2  26563  wilthlem3  26564  hhssnvt  30506  hhsssh  30510  foresf1o  31730  xrge0tsmsd  32197  gsumle  32230  esumsnf  33051  subfacp1lem3  34162  subfacp1lem5  34164  erdszelem1  34171  erdsze  34182  erdsze2lem2  34184  cvmscbv  34238  cvmshmeo  34251  cvmsss2  34254  eldm3  34720  dfrdg2  34756  bj-diagval  36044  mbfresfi  36523  disjresin  37095  elcoeleqvrels  37454  eleldisjs  37587  eldisjeq  37600  eqvrelqseqdisj3  37690  mzpcompact2lem  41475  seff  43054  wessf1ornlem  43868  fouriersw  44934  sge0tsms  45083  sge0f1o  45085  sge0sup  45094  meadjuni  45160  ismeannd  45170  psmeasurelem  45173  psmeasure  45174  omeunile  45208  isomennd  45234  hoidmvlelem3  45300