Theorem reseq2 5933

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 5638	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4172	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5636	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5636	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1541  Vcvv 3440   ∩ cin 3900   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908  df-opab 5161  df-xp 5630  df-res 5636

This theorem is referenced by:  reseq2i  5935  reseq2d  5938  resabs1  5965  resima2  5975  reldisjun  5991  imaeq2  6015  resdisj  6127  dfpo2  6254  fimadmfoALT  6757  fressnfv  7105  tfrlem1  8307  tfrlem9  8316  tfrlem11  8319  tfrlem12  8320  tfr2b  8327  tz7.44-1  8337  tz7.44-2  8338  tz7.44-3  8339  rdglem1  8346  fnfi  9102  fseqenlem1  9934  rtrclreclem4  14984  psgnprfval1  19451  gsumzaddlem  19850  gsum2dlem2  19900  gsumle  20074  znunithash  21519  islinds  21764  lmbr2  23203  lmff  23245  kgencn2  23501  ptcmpfi  23757  tsmsgsum  24083  tsmsres  24088  tsmsf1o  24089  tsmsxplem1  24097  tsmsxp  24099  ustval  24147  xrge0gsumle  24778  xrge0tsms  24779  lmmbr2  25215  lmcau  25269  limcun  25852  jensen  26955  wilthlem2  27035  wilthlem3  27036  hhssnvt  31340  hhsssh  31344  foresf1o  32579  xrge0tsmsd  33155  rprmdvdsprod  33615  esumsnf  34221  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem1  35385  erdsze  35396  erdsze2lem2  35398  cvmscbv  35452  cvmshmeo  35465  cvmsss2  35468  eldm3  35955  dfrdg2  35987  bj-diagval  37379  mbfresfi  37867  disjresin  38439  elcoeleqvrels  38852  eleldisjs  38987  eldisjeq  39000  eqvrelqseqdisj3  39090  mzpcompact2lem  42993  seff  44550  wessf1ornlem  45429  fouriersw  46475  sge0tsms  46624  sge0f1o  46626  sge0sup  46635  meadjuni  46701  ismeannd  46711  psmeasurelem  46714  psmeasure  46715  omeunile  46749  isomennd  46775  hoidmvlelem3  46841