Theorem reseq2 5941

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 5646	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4174	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5644	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5644	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1542  Vcvv 3442   ∩ cin 3902   × cxp 5630   ↾ cres 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910  df-opab 5163  df-xp 5638  df-res 5644

This theorem is referenced by:  reseq2i  5943  reseq2d  5946  resabs1  5973  resima2  5983  reldisjun  5999  imaeq2  6023  resdisj  6135  dfpo2  6262  fimadmfoALT  6765  fressnfv  7115  tfrlem1  8317  tfrlem9  8326  tfrlem11  8329  tfrlem12  8330  tfr2b  8337  tz7.44-1  8347  tz7.44-2  8348  tz7.44-3  8349  rdglem1  8356  fnfi  9114  fseqenlem1  9946  rtrclreclem4  14996  psgnprfval1  19463  gsumzaddlem  19862  gsum2dlem2  19912  gsumle  20086  znunithash  21531  islinds  21776  lmbr2  23215  lmff  23257  kgencn2  23513  ptcmpfi  23769  tsmsgsum  24095  tsmsres  24100  tsmsf1o  24101  tsmsxplem1  24109  tsmsxp  24111  ustval  24159  xrge0gsumle  24790  xrge0tsms  24791  lmmbr2  25227  lmcau  25281  limcun  25864  jensen  26967  wilthlem2  27047  wilthlem3  27048  hhssnvt  31352  hhsssh  31356  foresf1o  32590  xrge0tsmsd  33166  rprmdvdsprod  33626  esumsnf  34241  subfacp1lem3  35395  subfacp1lem5  35397  erdszelem1  35404  erdsze  35415  erdsze2lem2  35417  cvmscbv  35471  cvmshmeo  35484  cvmsss2  35487  eldm3  35974  dfrdg2  36006  bj-diagval  37426  mbfresfi  37914  disjresin  38491  elcoeleqvrels  38927  eleldisjs  39076  eldisjeq  39089  eqvrelqseqdisj3  39193  mzpcompact2lem  43105  seff  44662  wessf1ornlem  45541  fouriersw  46586  sge0tsms  46735  sge0f1o  46737  sge0sup  46746  meadjuni  46812  ismeannd  46822  psmeasurelem  46825  psmeasure  46826  omeunile  46860  isomennd  46886  hoidmvlelem3  46952