Theorem reseq2 5992

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 5699	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4220	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5697	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5697	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3480   ∩ cin 3950   × cxp 5683   ↾ cres 5687

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958  df-opab 5206  df-xp 5691  df-res 5697

This theorem is referenced by:  reseq2i  5994  reseq2d  5997  resabs1  6024  resima2  6034  reldisjun  6050  imaeq2  6074  resdisj  6189  dfpo2  6316  fimadmfoALT  6831  fressnfv  7180  tfrlem1  8416  tfrlem9  8425  tfrlem11  8428  tfrlem12  8429  tfr2b  8436  tz7.44-1  8446  tz7.44-2  8447  tz7.44-3  8448  rdglem1  8455  fnfi  9218  fseqenlem1  10064  rtrclreclem4  15100  psgnprfval1  19540  gsumzaddlem  19939  gsum2dlem2  19989  znunithash  21583  islinds  21829  lmbr2  23267  lmff  23309  kgencn2  23565  ptcmpfi  23821  tsmsgsum  24147  tsmsres  24152  tsmsf1o  24153  tsmsxplem1  24161  tsmsxp  24163  ustval  24211  xrge0gsumle  24855  xrge0tsms  24856  lmmbr2  25293  lmcau  25347  limcun  25930  jensen  27032  wilthlem2  27112  wilthlem3  27113  hhssnvt  31284  hhsssh  31288  foresf1o  32523  xrge0tsmsd  33065  gsumle  33101  rprmdvdsprod  33562  esumsnf  34065  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem1  35196  erdsze  35207  erdsze2lem2  35209  cvmscbv  35263  cvmshmeo  35276  cvmsss2  35279  eldm3  35761  dfrdg2  35796  bj-diagval  37175  mbfresfi  37673  disjresin  38241  elcoeleqvrels  38596  eleldisjs  38729  eldisjeq  38742  eqvrelqseqdisj3  38832  mzpcompact2lem  42762  seff  44328  wessf1ornlem  45190  fouriersw  46246  sge0tsms  46395  sge0f1o  46397  sge0sup  46406  meadjuni  46472  ismeannd  46482  psmeasurelem  46485  psmeasure  46486  omeunile  46520  isomennd  46546  hoidmvlelem3  46612