Theorem reseq2 5875

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 5594	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4143	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5592	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5592	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1539  Vcvv 3422   ∩ cin 3882   × cxp 5578   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890  df-opab 5133  df-xp 5586  df-res 5592

This theorem is referenced by:  reseq2i  5877  reseq2d  5880  resabs1  5910  resima2  5915  imaeq2  5954  resdisj  6061  dfpo2  6188  fimadmfoALT  6683  fressnfv  7014  tfrlem1  8178  tfrlem9  8187  tfrlem11  8190  tfrlem12  8191  tfr2b  8198  tz7.44-1  8208  tz7.44-2  8209  tz7.44-3  8210  rdglem1  8217  fnfi  8925  fseqenlem1  9711  rtrclreclem4  14700  psgnprfval1  19045  gsumzaddlem  19437  gsum2dlem2  19487  znunithash  20684  islinds  20926  lmbr2  22318  lmff  22360  kgencn2  22616  ptcmpfi  22872  tsmsgsum  23198  tsmsres  23203  tsmsf1o  23204  tsmsxplem1  23212  tsmsxp  23214  ustval  23262  xrge0gsumle  23902  xrge0tsms  23903  lmmbr2  24328  lmcau  24382  limcun  24964  jensen  26043  wilthlem2  26123  wilthlem3  26124  hhssnvt  29528  hhsssh  29532  foresf1o  30751  reldisjun  30843  xrge0tsmsd  31219  gsumle  31252  esumsnf  31932  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem1  33053  erdsze  33064  erdsze2lem2  33066  cvmscbv  33120  cvmshmeo  33133  cvmsss2  33136  eldm3  33634  dfrdg2  33677  bj-diagval  35272  mbfresfi  35750  elcoeleqvrels  36635  eleldisjs  36766  eldisjeq  36779  mzpcompact2lem  40489  seff  41816  wessf1ornlem  42611  fouriersw  43662  sge0tsms  43808  sge0f1o  43810  sge0sup  43819  meadjuni  43885  ismeannd  43895  psmeasurelem  43898  psmeasure  43899  omeunile  43933  isomennd  43959  hoidmvlelem3  44025