Theorem reseq2 5312

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 5052	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 3776	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5050	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5050	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1475  Vcvv 3173   ∩ cin 3539   × cxp 5036   ↾ cres 5040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-opab 4644  df-xp 5044  df-res 5050

This theorem is referenced by:  reseq2i  5314  reseq2d  5317  resabs1  5347  resima2  5352  resima2OLD  5353  imaeq2  5381  resdisj  5482  fressnfv  6332  tfrlem1  7359  tfrlem9  7368  tfrlem11  7371  tfrlem12  7372  tfr2b  7379  tz7.44-1  7389  tz7.44-2  7390  tz7.44-3  7391  rdglem1  7398  fnfi  8123  fseqenlem1  8730  rtrclreclem4  13649  psgnprfval1  17765  gsumzaddlem  18144  gsum2dlem2  18193  znunithash  19732  islinds  19967  lmbr2  20873  lmff  20915  kgencn2  21170  ptcmpfi  21426  tsmsgsum  21752  tsmsres  21757  tsmsf1o  21758  tsmsxplem1  21766  tsmsxp  21768  ustval  21816  xrge0gsumle  22444  xrge0tsms  22445  lmmbr2  22865  lmcau  22919  limcun  23465  jensen  24515  wilthlem2  24595  wilthlem3  24596  hhssnvt  27506  hhsssh  27510  foresf1o  28727  gsumle  29110  xrge0tsmsd  29116  esumsnf  29453  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem1  30427  erdsze  30438  erdsze2lem2  30440  cvmscbv  30494  cvmshmeo  30507  cvmsss2  30510  dfpo2  30898  eldm3  30905  dfrdg2  30945  nofulllem4  31104  nofulllem5  31105  mbfresfi  32626  mzpcompact2lem  36332  seff  37530  wessf1ornlem  38366  fouriersw  39124  sge0tsms  39273  sge0f1o  39275  sge0sup  39284  meadjuni  39350  ismeannd  39360  psmeasurelem  39363  psmeasure  39364  omeunile  39395  isomennd  39421  hoidmvlelem3  39487