Theorem reseq2 6004

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 5714	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
2	1	ineq2d 4241	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3		df-res 5712	. 2 ⊢ (𝐶 ↾ 𝐴) = (𝐶 ∩ (𝐴 × V))
4		df-res 5712	. 2 ⊢ (𝐶 ↾ 𝐵) = (𝐶 ∩ (𝐵 × V))
5	2, 3, 4	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))

Syntax hints:   → wi 4   = wceq 1537  Vcvv 3488   ∩ cin 3975   × cxp 5698   ↾ cres 5702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983  df-opab 5229  df-xp 5706  df-res 5712

This theorem is referenced by:  reseq2i  6006  reseq2d  6009  resabs1  6036  resima2  6045  reldisjun  6061  imaeq2  6085  resdisj  6200  dfpo2  6327  fimadmfoALT  6845  fressnfv  7194  tfrlem1  8432  tfrlem9  8441  tfrlem11  8444  tfrlem12  8445  tfr2b  8452  tz7.44-1  8462  tz7.44-2  8463  tz7.44-3  8464  rdglem1  8471  fnfi  9244  fseqenlem1  10093  rtrclreclem4  15110  psgnprfval1  19564  gsumzaddlem  19963  gsum2dlem2  20013  znunithash  21606  islinds  21852  lmbr2  23288  lmff  23330  kgencn2  23586  ptcmpfi  23842  tsmsgsum  24168  tsmsres  24173  tsmsf1o  24174  tsmsxplem1  24182  tsmsxp  24184  ustval  24232  xrge0gsumle  24874  xrge0tsms  24875  lmmbr2  25312  lmcau  25366  limcun  25950  jensen  27050  wilthlem2  27130  wilthlem3  27131  hhssnvt  31297  hhsssh  31301  foresf1o  32532  xrge0tsmsd  33041  gsumle  33074  rprmdvdsprod  33527  esumsnf  34028  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem1  35159  erdsze  35170  erdsze2lem2  35172  cvmscbv  35226  cvmshmeo  35239  cvmsss2  35242  eldm3  35723  dfrdg2  35759  bj-diagval  37140  mbfresfi  37626  disjresin  38195  elcoeleqvrels  38551  eleldisjs  38684  eldisjeq  38697  eqvrelqseqdisj3  38787  mzpcompact2lem  42707  seff  44278  wessf1ornlem  45092  fouriersw  46152  sge0tsms  46301  sge0f1o  46303  sge0sup  46312  meadjuni  46378  ismeannd  46388  psmeasurelem  46391  psmeasure  46392  omeunile  46426  isomennd  46452  hoidmvlelem3  46518