MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reseq2 Structured version   Visualization version   GIF version

Theorem reseq2 5937
Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994.)
Assertion
Ref Expression
reseq2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5652 . . 3 (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
21ineq2d 4177 . 2 (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3 df-res 5650 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
4 df-res 5650 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
52, 3, 43eqtr4g 2802 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  Vcvv 3448  cin 3914   × cxp 5636  cres 5640
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-in 3922  df-opab 5173  df-xp 5644  df-res 5650
This theorem is referenced by:  reseq2i  5939  reseq2d  5942  resabs1  5972  resima2  5977  imaeq2  6014  resdisj  6126  dfpo2  6253  fimadmfoALT  6772  fressnfv  7111  tfrlem1  8327  tfrlem9  8336  tfrlem11  8339  tfrlem12  8340  tfr2b  8347  tz7.44-1  8357  tz7.44-2  8358  tz7.44-3  8359  rdglem1  8366  fnfi  9132  fseqenlem1  9967  rtrclreclem4  14953  psgnprfval1  19311  gsumzaddlem  19705  gsum2dlem2  19755  znunithash  20987  islinds  21231  lmbr2  22626  lmff  22668  kgencn2  22924  ptcmpfi  23180  tsmsgsum  23506  tsmsres  23511  tsmsf1o  23512  tsmsxplem1  23520  tsmsxp  23522  ustval  23570  xrge0gsumle  24212  xrge0tsms  24213  lmmbr2  24639  lmcau  24693  limcun  25275  jensen  26354  wilthlem2  26434  wilthlem3  26435  hhssnvt  30249  hhsssh  30253  foresf1o  31473  reldisjun  31563  xrge0tsmsd  31941  gsumle  31974  esumsnf  32703  subfacp1lem3  33816  subfacp1lem5  33818  erdszelem1  33825  erdsze  33836  erdsze2lem2  33838  cvmscbv  33892  cvmshmeo  33905  cvmsss2  33908  eldm3  34373  dfrdg2  34409  bj-diagval  35674  mbfresfi  36153  disjresin  36726  elcoeleqvrels  37086  eleldisjs  37219  eldisjeq  37232  eqvrelqseqdisj3  37322  mzpcompact2lem  41103  seff  42663  wessf1ornlem  43477  fouriersw  44546  sge0tsms  44695  sge0f1o  44697  sge0sup  44706  meadjuni  44772  ismeannd  44782  psmeasurelem  44785  psmeasure  44786  omeunile  44820  isomennd  44846  hoidmvlelem3  44912
  Copyright terms: Public domain W3C validator