Theorem reseq2 5628

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 5360	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4043	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5358	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5358	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2886	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1656  Vcvv 3414   ∩ cin 3797   × cxp 5344   ↾ cres 5348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-opab 4938  df-xp 5352  df-res 5358

This theorem is referenced by:  reseq2i  5630  reseq2d  5633  resabs1  5667  resima2  5672  imaeq2  5707  resdisj  5808  fimadmfoALT  6368  fressnfv  6683  tfrlem1  7743  tfrlem9  7752  tfrlem11  7755  tfrlem12  7756  tfr2b  7763  tz7.44-1  7773  tz7.44-2  7774  tz7.44-3  7775  rdglem1  7782  fnfi  8513  fseqenlem1  9167  rtrclreclem4  14185  psgnprfval1  18300  gsumzaddlem  18681  gsum2dlem2  18730  znunithash  20279  islinds  20522  lmbr2  21441  lmff  21483  kgencn2  21738  ptcmpfi  21994  tsmsgsum  22319  tsmsres  22324  tsmsf1o  22325  tsmsxplem1  22333  tsmsxp  22335  ustval  22383  xrge0gsumle  23013  xrge0tsms  23014  lmmbr2  23434  lmcau  23488  limcun  24065  jensen  25135  wilthlem2  25215  wilthlem3  25216  hhssnvt  28673  hhsssh  28677  foresf1o  29887  gsumle  30320  xrge0tsmsd  30326  esumsnf  30667  subfacp1lem3  31706  subfacp1lem5  31708  erdszelem1  31715  erdsze  31726  erdsze2lem2  31728  cvmscbv  31782  cvmshmeo  31795  cvmsss2  31798  dfpo2  32183  eldm3  32189  dfrdg2  32234  mbfresfi  33998  mzpcompact2lem  38157  seff  39347  wessf1ornlem  40178  fouriersw  41240  sge0tsms  41386  sge0f1o  41388  sge0sup  41397  meadjuni  41463  ismeannd  41473  psmeasurelem  41476  psmeasure  41477  omeunile  41511  isomennd  41537  hoidmvlelem3  41603