Theorem reseq2 5945

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 5652	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4183	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5650	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5650	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  Vcvv 3447   ∩ cin 3913   × cxp 5636   ↾ cres 5640

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-in 3921  df-opab 5170  df-xp 5644  df-res 5650

This theorem is referenced by:  reseq2i  5947  reseq2d  5950  resabs1  5977  resima2  5987  reldisjun  6003  imaeq2  6027  resdisj  6142  dfpo2  6269  fimadmfoALT  6783  fressnfv  7132  tfrlem1  8344  tfrlem9  8353  tfrlem11  8356  tfrlem12  8357  tfr2b  8364  tz7.44-1  8374  tz7.44-2  8375  tz7.44-3  8376  rdglem1  8383  fnfi  9142  fseqenlem1  9977  rtrclreclem4  15027  psgnprfval1  19452  gsumzaddlem  19851  gsum2dlem2  19901  znunithash  21474  islinds  21718  lmbr2  23146  lmff  23188  kgencn2  23444  ptcmpfi  23700  tsmsgsum  24026  tsmsres  24031  tsmsf1o  24032  tsmsxplem1  24040  tsmsxp  24042  ustval  24090  xrge0gsumle  24722  xrge0tsms  24723  lmmbr2  25159  lmcau  25213  limcun  25796  jensen  26899  wilthlem2  26979  wilthlem3  26980  hhssnvt  31194  hhsssh  31198  foresf1o  32433  xrge0tsmsd  33002  gsumle  33038  rprmdvdsprod  33505  esumsnf  34054  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem1  35178  erdsze  35189  erdsze2lem2  35191  cvmscbv  35245  cvmshmeo  35258  cvmsss2  35261  eldm3  35748  dfrdg2  35783  bj-diagval  37162  mbfresfi  37660  disjresin  38228  elcoeleqvrels  38586  eleldisjs  38720  eldisjeq  38733  eqvrelqseqdisj3  38823  mzpcompact2lem  42739  seff  44298  wessf1ornlem  45179  fouriersw  46229  sge0tsms  46378  sge0f1o  46380  sge0sup  46389  meadjuni  46455  ismeannd  46465  psmeasurelem  46468  psmeasure  46469  omeunile  46503  isomennd  46529  hoidmvlelem3  46595