Theorem reseq2 5971

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 5673	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4181	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5671	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5671	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2829	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1567  Vcvv 3463   ∩ cin 3912   × cxp 5657   ↾ cres 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920  df-opab 5175  df-xp 5665  df-res 5671

This theorem is referenced by:  reseq2i  5973  reseq2d  5976  resabs1  6003  resima2  6013  reldmun  6031  reldisjunOLD  6032  imaeq2  6056  resdisj  6166  dfpo2  6294  fimadmfoALT  6801  fressnfv  7155  tfrlem1  8358  tfrlem9  8368  tfrlem11  8371  tfrlem12  8372  tfr2b  8379  tz7.44-1  8389  tz7.44-2  8390  tz7.44-3  8391  rdglem1  8398  fnfi  9158  fseqenlem1  10004  rtrclreclem4  15094  psgnprfval1  19588  gsumzaddlem  19987  gsum2dlem2  20037  gsumle  20211  znunithash  21679  islinds  21924  lmbr2  23381  lmff  23423  kgencn2  23679  ptcmpfi  23935  tsmsgsum  24261  tsmsres  24266  tsmsf1o  24267  tsmsxplem1  24275  tsmsxp  24277  ustval  24325  xrge0gsumle  24956  xrge0tsms  24957  lmmbr2  25383  lmcau  25437  limcun  26019  jensen  27115  wilthlem2  27195  wilthlem3  27196  hhssnvt  31554  hhsssh  31558  foresf1o  32787  xrge0tsmsd  33330  rprmdvdsprod  33765  esumsnf  34395  subfacp1lem3  35569  subfacp1lem5  35571  erdszelem1  35578  erdsze  35589  erdsze2lem2  35591  cvmscbv  35645  cvmshmeo  35658  cvmsss2  35661  eldm3  36148  dfrdg2  36180  bj-diagval  37701  mbfresfi  38200  disjresin  38777  elcoeleqvrels  39213  eleldisjs  39362  eldisjeq  39375  eqvrelqseqdisj3  39479  mzpcompact2lem  43367  seff  44904  wessf1ornlem  45788  fouriersw  46830  sge0tsms  46979  sge0f1o  46981  sge0sup  46990  meadjuni  47056  ismeannd  47066  psmeasurelem  47069  psmeasure  47070  omeunile  47104  isomennd  47130  hoidmvlelem3  47196