Theorem reseq2 5948

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 5655	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4186	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5653	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5653	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3450   ∩ cin 3916   × cxp 5639   ↾ cres 5643

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-in 3924  df-opab 5173  df-xp 5647  df-res 5653

This theorem is referenced by:  reseq2i  5950  reseq2d  5953  resabs1  5980  resima2  5990  reldisjun  6006  imaeq2  6030  resdisj  6145  dfpo2  6272  fimadmfoALT  6786  fressnfv  7135  tfrlem1  8347  tfrlem9  8356  tfrlem11  8359  tfrlem12  8360  tfr2b  8367  tz7.44-1  8377  tz7.44-2  8378  tz7.44-3  8379  rdglem1  8386  fnfi  9148  fseqenlem1  9984  rtrclreclem4  15034  psgnprfval1  19459  gsumzaddlem  19858  gsum2dlem2  19908  znunithash  21481  islinds  21725  lmbr2  23153  lmff  23195  kgencn2  23451  ptcmpfi  23707  tsmsgsum  24033  tsmsres  24038  tsmsf1o  24039  tsmsxplem1  24047  tsmsxp  24049  ustval  24097  xrge0gsumle  24729  xrge0tsms  24730  lmmbr2  25166  lmcau  25220  limcun  25803  jensen  26906  wilthlem2  26986  wilthlem3  26987  hhssnvt  31201  hhsssh  31205  foresf1o  32440  xrge0tsmsd  33009  gsumle  33045  rprmdvdsprod  33512  esumsnf  34061  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem1  35185  erdsze  35196  erdsze2lem2  35198  cvmscbv  35252  cvmshmeo  35265  cvmsss2  35268  eldm3  35755  dfrdg2  35790  bj-diagval  37169  mbfresfi  37667  disjresin  38235  elcoeleqvrels  38593  eleldisjs  38727  eldisjeq  38740  eqvrelqseqdisj3  38830  mzpcompact2lem  42746  seff  44305  wessf1ornlem  45186  fouriersw  46236  sge0tsms  46385  sge0f1o  46387  sge0sup  46396  meadjuni  46462  ismeannd  46472  psmeasurelem  46475  psmeasure  46476  omeunile  46510  isomennd  46536  hoidmvlelem3  46602