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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3457   ∩ cin 3905   × cxp 5661   ↾ cres 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-in 3913  df-opab 5176  df-xp 5669  df-res 5675

This theorem is used by:  reseq2i  5977  reseq2d  5980  resabs1  6007  resima2  6017  reldmun  6035  reldisjunOLD  6036  imaeq2  6060  resdisj  6169  dfpo2  6301  fimadmfoALT  6807  fressnfv  7161  tfrlem1  8364  tfrlem9  8374  tfrlem11  8377  tfrlem12  8378  tfr2b  8385  tz7.44-1  8395  tz7.44-2  8396  tz7.44-3  8397  rdglem1  8404  fnfi  9165  fseqenlem1  10020  rtrclreclem4  15117  psgnprfval1  19615  gsumzaddlem  20014  gsum2dlem2  20064  gsumle  20238  znunithash  21743  islinds  21988  lmbr2  23445  lmff  23487  kgencn2  23743  ptcmpfi  23999  tsmsgsum  24325  tsmsres  24330  tsmsf1o  24331  tsmsxplem1  24339  tsmsxp  24341  ustval  24389  xrge0gsumle  25020  xrge0tsms  25021  lmmbr2  25447  lmcau  25501  limcun  26083  jensen  27182  wilthlem2  27262  wilthlem3  27263  hhssnvt  31646  hhsssh  31650  foresf1o  32879  xrge0tsmsd  33416  rprmdvdsprod  33847  esumsnf  34477  subfacp1lem3  35687  subfacp1lem5  35689  erdszelem1  35696  erdsze  35707  erdsze2lem2  35709  cvmscbv  35763  cvmshmeo  35776  cvmsss2  35779  eldm3  36266  dfrdg2  36298  bj-diagval  37851  mbfresfi  38350  disjresin  38925  elcoeleqvrels  39361  eleldisjs  39510  eldisjeq  39523  eqvrelqseqdisj3  39627  mzpcompact2lem  43515  seff  45052  wessf1ornlem  45936  fouriersw  46978  sge0tsms  47127  sge0f1o  47129  sge0sup  47138  meadjuni  47204  ismeannd  47214  psmeasurelem  47217  psmeasure  47218  omeunile  47252  isomennd  47278  hoidmvlelem3  47344