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

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

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5263 . . 3 (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
21ineq2d 3965 . 2 (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3 df-res 5261 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
4 df-res 5261 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
52, 3, 43eqtr4g 2830 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  Vcvv 3351  cin 3722   × cxp 5247  cres 5251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-opab 4847  df-xp 5255  df-res 5261
This theorem is referenced by:  reseq2i  5531  reseq2d  5534  resabs1  5568  resima2  5573  resima2OLD  5574  imaeq2  5603  resdisj  5704  fressnfv  6570  tfrlem1  7625  tfrlem9  7634  tfrlem11  7637  tfrlem12  7638  tfr2b  7645  tz7.44-1  7655  tz7.44-2  7656  tz7.44-3  7657  rdglem1  7664  fnfi  8394  fseqenlem1  9047  rtrclreclem4  14009  psgnprfval1  18149  gsumzaddlem  18528  gsum2dlem2  18577  znunithash  20128  islinds  20365  lmbr2  21284  lmff  21326  kgencn2  21581  ptcmpfi  21837  tsmsgsum  22162  tsmsres  22167  tsmsf1o  22168  tsmsxplem1  22176  tsmsxp  22178  ustval  22226  xrge0gsumle  22856  xrge0tsms  22857  lmmbr2  23276  lmcau  23330  limcun  23879  jensen  24936  wilthlem2  25016  wilthlem3  25017  hhssnvt  28462  hhsssh  28466  foresf1o  29681  gsumle  30119  xrge0tsmsd  30125  esumsnf  30466  subfacp1lem3  31502  subfacp1lem5  31504  erdszelem1  31511  erdsze  31522  erdsze2lem2  31524  cvmscbv  31578  cvmshmeo  31591  cvmsss2  31594  dfpo2  31983  eldm3  31989  dfrdg2  32037  mbfresfi  33788  mzpcompact2lem  37840  seff  39034  wessf1ornlem  39891  fouriersw  40965  sge0tsms  41114  sge0f1o  41116  sge0sup  41125  meadjuni  41191  ismeannd  41201  psmeasurelem  41204  psmeasure  41205  omeunile  41239  isomennd  41265  hoidmvlelem3  41331
  Copyright terms: Public domain W3C validator