Theorem reseq2 5977

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

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3475   ∩ cin 3948   × cxp 5675   ↾ cres 5679

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 3956  df-opab 5212  df-xp 5683  df-res 5689

This theorem is referenced by:  reseq2i  5979  reseq2d  5982  resabs1  6012  resima2  6017  reldisjun  6033  imaeq2  6056  resdisj  6169  dfpo2  6296  fimadmfoALT  6817  fressnfv  7158  tfrlem1  8376  tfrlem9  8385  tfrlem11  8388  tfrlem12  8389  tfr2b  8396  tz7.44-1  8406  tz7.44-2  8407  tz7.44-3  8408  rdglem1  8415  fnfi  9181  fseqenlem1  10019  rtrclreclem4  15008  psgnprfval1  19390  gsumzaddlem  19789  gsum2dlem2  19839  znunithash  21120  islinds  21364  lmbr2  22763  lmff  22805  kgencn2  23061  ptcmpfi  23317  tsmsgsum  23643  tsmsres  23648  tsmsf1o  23649  tsmsxplem1  23657  tsmsxp  23659  ustval  23707  xrge0gsumle  24349  xrge0tsms  24350  lmmbr2  24776  lmcau  24830  limcun  25412  jensen  26493  wilthlem2  26573  wilthlem3  26574  hhssnvt  30518  hhsssh  30522  foresf1o  31742  xrge0tsmsd  32209  gsumle  32242  esumsnf  33062  subfacp1lem3  34173  subfacp1lem5  34175  erdszelem1  34182  erdsze  34193  erdsze2lem2  34195  cvmscbv  34249  cvmshmeo  34262  cvmsss2  34265  eldm3  34731  dfrdg2  34767  bj-diagval  36055  mbfresfi  36534  disjresin  37106  elcoeleqvrels  37465  eleldisjs  37598  eldisjeq  37611  eqvrelqseqdisj3  37701  mzpcompact2lem  41489  seff  43068  wessf1ornlem  43882  fouriersw  44947  sge0tsms  45096  sge0f1o  45098  sge0sup  45107  meadjuni  45173  ismeannd  45183  psmeasurelem  45186  psmeasure  45187  omeunile  45221  isomennd  45247  hoidmvlelem3  45313