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

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

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5037 . . 3 (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
21ineq2d 3770 . 2 (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3 df-res 5035 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
4 df-res 5035 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
52, 3, 43eqtr4g 2663 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  Vcvv 3167  cin 3533   × cxp 5021  cres 5025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-v 3169  df-in 3541  df-opab 4633  df-xp 5029  df-res 5035
This theorem is referenced by:  reseq2i  5296  reseq2d  5299  resabs1  5329  resima2  5334  resima2OLD  5335  imaeq2  5363  resdisj  5463  fressnfv  6305  tfrlem1  7331  tfrlem9  7340  tfrlem11  7343  tfrlem12  7344  tfr2b  7351  tz7.44-1  7361  tz7.44-2  7362  tz7.44-3  7363  rdglem1  7370  fnfi  8095  fseqenlem1  8702  rtrclreclem4  13590  psgnprfval1  17706  gsumzaddlem  18085  gsum2dlem2  18134  znunithash  19672  islinds  19904  lmbr2  20810  lmff  20852  kgencn2  21107  ptcmpfi  21363  tsmsgsum  21689  tsmsres  21694  tsmsf1o  21695  tsmsxplem1  21703  tsmsxp  21705  ustval  21753  xrge0gsumle  22371  xrge0tsms  22372  lmmbr2  22778  lmcau  22831  limcun  23377  jensen  24427  wilthlem2  24507  wilthlem3  24508  hhssnvt  27307  hhsssh  27311  foresf1o  28528  gsumle  28911  xrge0tsmsd  28917  esumsnf  29254  subfacp1lem3  30219  subfacp1lem5  30221  erdszelem1  30228  erdsze  30239  erdsze2lem2  30241  cvmscbv  30295  cvmshmeo  30308  cvmsss2  30311  dfpo2  30699  eldm3  30706  dfrdg2  30746  nofulllem4  30905  nofulllem5  30906  mbfresfi  32424  mzpcompact2lem  36130  seff  37328  wessf1ornlem  38164  fouriersw  38923  sge0tsms  39072  sge0f1o  39074  sge0sup  39083  meadjuni  39149  ismeannd  39159  psmeasurelem  39162  psmeasure  39163  omeunile  39194  isomennd  39220  hoidmvlelem3  39286
  Copyright terms: Public domain W3C validator