Theorem reseq2 5886

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 5603	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4146	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5601	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5601	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1539  Vcvv 3432   ∩ cin 3886   × cxp 5587   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-in 3894  df-opab 5137  df-xp 5595  df-res 5601

This theorem is referenced by:  reseq2i  5888  reseq2d  5891  resabs1  5921  resima2  5926  imaeq2  5965  resdisj  6072  dfpo2  6199  fimadmfoALT  6699  fressnfv  7032  tfrlem1  8207  tfrlem9  8216  tfrlem11  8219  tfrlem12  8220  tfr2b  8227  tz7.44-1  8237  tz7.44-2  8238  tz7.44-3  8239  rdglem1  8246  fnfi  8964  fseqenlem1  9780  rtrclreclem4  14772  psgnprfval1  19130  gsumzaddlem  19522  gsum2dlem2  19572  znunithash  20772  islinds  21016  lmbr2  22410  lmff  22452  kgencn2  22708  ptcmpfi  22964  tsmsgsum  23290  tsmsres  23295  tsmsf1o  23296  tsmsxplem1  23304  tsmsxp  23306  ustval  23354  xrge0gsumle  23996  xrge0tsms  23997  lmmbr2  24423  lmcau  24477  limcun  25059  jensen  26138  wilthlem2  26218  wilthlem3  26219  hhssnvt  29627  hhsssh  29631  foresf1o  30850  reldisjun  30942  xrge0tsmsd  31317  gsumle  31350  esumsnf  32032  subfacp1lem3  33144  subfacp1lem5  33146  erdszelem1  33153  erdsze  33164  erdsze2lem2  33166  cvmscbv  33220  cvmshmeo  33233  cvmsss2  33236  eldm3  33728  dfrdg2  33771  bj-diagval  35345  mbfresfi  35823  elcoeleqvrels  36708  eleldisjs  36839  eldisjeq  36852  mzpcompact2lem  40573  seff  41927  wessf1ornlem  42722  fouriersw  43772  sge0tsms  43918  sge0f1o  43920  sge0sup  43929  meadjuni  43995  ismeannd  44005  psmeasurelem  44008  psmeasure  44009  omeunile  44043  isomennd  44069  hoidmvlelem3  44135