Theorem reseq2 5979

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 5670	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4120	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5668	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5668	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  Vcvv 3454   ∩ cin 4092   × cxp 5654   ↾ cres 5658

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094  df-opab 5172  df-xp 5662  df-res 5668

This theorem is used by:  reseq2i  5981  reseq2d  5984  resabs1  6012  reldmun  6039  reldisjunOLD  6040  imaeq2  6064  resima2  6073  resdisj  6177  dfpo2  6323  fimadmfoALT  6835  fressnfv  7194  tfrlem1  8419  tfrlem9  8429  tfrlem11  8432  tfrlem12  8433  tfr2b  8440  tz7.44-1  8450  tz7.44-2  8451  tz7.44-3  8452  rdglem1  8459  fnfi  9229  fseqenlem1  10140  rtrclreclem4  15255  psgnprfval1  19778  gsumzaddlem  20177  gsum2dlem2  20227  gsumle  20401  znunithash  21914  islinds  22159  lmbr2  23621  lmff  23663  kgencn2  23920  ptcmpfi  24176  tsmsgsum  24502  tsmsres  24507  tsmsf1o  24508  tsmsxplem1  24516  tsmsxp  24518  ustval  24566  xrge0gsumle  25197  xrge0tsms  25198  lmmbr2  25624  lmcau  25678  limcun  26259  jensen  27362  wilthlem2  27442  wilthlem3  27443  hhssnvt  31913  hhsssh  31917  foresf1o  33188  xrge0tsmsd  33723  rprmdvdsprod  34163  esumsnf  34800  gdlop4fv  36000  subfacp1lem3  36148  subfacp1lem5  36150  erdszelem1  36157  erdsze  36168  erdsze2lem2  36170  cvmscbv  36224  cvmshmeo  36237  cvmsss2  36240  eldm3  36734  dfrdg2  36765  bj-diagval  38356  mbfresfi  38845  disjresin  39434  elcoeleqvrels  39870  eleldisjs  40019  eldisjeq  40032  eqvrelqseqdisj3  40136  mzpcompact2lem  44022  seff  45548  wessf1ornlem  46467  fouriersw  47508  sge0tsms  47657  sge0f1o  47659  sge0sup  47668  meadjuni  47734  ismeannd  47744  psmeasurelem  47747  psmeasure  47748  omeunile  47782  isomennd  47808  hoidmvlelem3  47874