Theorem reseq2 5929

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 5637	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4173	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5635	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5635	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3438   ∩ cin 3904   × cxp 5621   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912  df-opab 5158  df-xp 5629  df-res 5635

This theorem is referenced by:  reseq2i  5931  reseq2d  5934  resabs1  5961  resima2  5971  reldisjun  5987  imaeq2  6011  resdisj  6122  dfpo2  6248  fimadmfoALT  6751  fressnfv  7098  tfrlem1  8305  tfrlem9  8314  tfrlem11  8317  tfrlem12  8318  tfr2b  8325  tz7.44-1  8335  tz7.44-2  8336  tz7.44-3  8337  rdglem1  8344  fnfi  9102  fseqenlem1  9937  rtrclreclem4  14986  psgnprfval1  19419  gsumzaddlem  19818  gsum2dlem2  19868  gsumle  20042  znunithash  21489  islinds  21734  lmbr2  23162  lmff  23204  kgencn2  23460  ptcmpfi  23716  tsmsgsum  24042  tsmsres  24047  tsmsf1o  24048  tsmsxplem1  24056  tsmsxp  24058  ustval  24106  xrge0gsumle  24738  xrge0tsms  24739  lmmbr2  25175  lmcau  25229  limcun  25812  jensen  26915  wilthlem2  26995  wilthlem3  26996  hhssnvt  31227  hhsssh  31231  foresf1o  32466  xrge0tsmsd  33028  rprmdvdsprod  33484  esumsnf  34033  subfacp1lem3  35157  subfacp1lem5  35159  erdszelem1  35166  erdsze  35177  erdsze2lem2  35179  cvmscbv  35233  cvmshmeo  35246  cvmsss2  35249  eldm3  35736  dfrdg2  35771  bj-diagval  37150  mbfresfi  37648  disjresin  38216  elcoeleqvrels  38574  eleldisjs  38708  eldisjeq  38721  eqvrelqseqdisj3  38811  mzpcompact2lem  42727  seff  44285  wessf1ornlem  45166  fouriersw  46216  sge0tsms  46365  sge0f1o  46367  sge0sup  46376  meadjuni  46442  ismeannd  46452  psmeasurelem  46455  psmeasure  46456  omeunile  46490  isomennd  46516  hoidmvlelem3  46582