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

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

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5126 . . 3 (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
21ineq2d 3812 . 2 (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3 df-res 5124 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
4 df-res 5124 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
52, 3, 43eqtr4g 2680 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  Vcvv 3198  cin 3571   × cxp 5110  cres 5114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-opab 4711  df-xp 5118  df-res 5124
This theorem is referenced by:  reseq2i  5391  reseq2d  5394  resabs1  5425  resima2  5430  resima2OLD  5431  imaeq2  5460  resdisj  5561  fressnfv  6424  tfrlem1  7469  tfrlem9  7478  tfrlem11  7481  tfrlem12  7482  tfr2b  7489  tz7.44-1  7499  tz7.44-2  7500  tz7.44-3  7501  rdglem1  7508  fnfi  8235  fseqenlem1  8844  rtrclreclem4  13795  psgnprfval1  17936  gsumzaddlem  18315  gsum2dlem2  18364  znunithash  19907  islinds  20142  lmbr2  21057  lmff  21099  kgencn2  21354  ptcmpfi  21610  tsmsgsum  21936  tsmsres  21941  tsmsf1o  21942  tsmsxplem1  21950  tsmsxp  21952  ustval  22000  xrge0gsumle  22630  xrge0tsms  22631  lmmbr2  23051  lmcau  23105  limcun  23653  jensen  24709  wilthlem2  24789  wilthlem3  24790  hhssnvt  28106  hhsssh  28110  foresf1o  29327  gsumle  29764  xrge0tsmsd  29770  esumsnf  30111  subfacp1lem3  31149  subfacp1lem5  31151  erdszelem1  31158  erdsze  31169  erdsze2lem2  31171  cvmscbv  31225  cvmshmeo  31238  cvmsss2  31241  dfpo2  31631  eldm3  31637  dfrdg2  31685  mbfresfi  33436  mzpcompact2lem  37140  seff  38334  wessf1ornlem  39193  fouriersw  40217  sge0tsms  40366  sge0f1o  40368  sge0sup  40377  meadjuni  40443  ismeannd  40453  psmeasurelem  40456  psmeasure  40457  omeunile  40488  isomennd  40514  hoidmvlelem3  40580
  Copyright terms: Public domain W3C validator