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

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

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5118 . . 3 (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
21ineq2d 3806 . 2 (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3 df-res 5116 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
4 df-res 5116 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
52, 3, 43eqtr4g 2679 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  Vcvv 3195  cin 3566   × cxp 5102  cres 5106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-opab 4704  df-xp 5110  df-res 5116
This theorem is referenced by:  reseq2i  5382  reseq2d  5385  resabs1  5415  resima2  5420  resima2OLD  5421  imaeq2  5450  resdisj  5551  fressnfv  6412  tfrlem1  7457  tfrlem9  7466  tfrlem11  7469  tfrlem12  7470  tfr2b  7477  tz7.44-1  7487  tz7.44-2  7488  tz7.44-3  7489  rdglem1  7496  fnfi  8223  fseqenlem1  8832  rtrclreclem4  13782  psgnprfval1  17923  gsumzaddlem  18302  gsum2dlem2  18351  znunithash  19894  islinds  20129  lmbr2  21044  lmff  21086  kgencn2  21341  ptcmpfi  21597  tsmsgsum  21923  tsmsres  21928  tsmsf1o  21929  tsmsxplem1  21937  tsmsxp  21939  ustval  21987  xrge0gsumle  22617  xrge0tsms  22618  lmmbr2  23038  lmcau  23092  limcun  23640  jensen  24696  wilthlem2  24776  wilthlem3  24777  hhssnvt  28092  hhsssh  28096  foresf1o  29315  gsumle  29753  xrge0tsmsd  29759  esumsnf  30100  subfacp1lem3  31138  subfacp1lem5  31140  erdszelem1  31147  erdsze  31158  erdsze2lem2  31160  cvmscbv  31214  cvmshmeo  31227  cvmsss2  31230  dfpo2  31620  eldm3  31627  dfrdg2  31675  mbfresfi  33427  mzpcompact2lem  37133  seff  38328  wessf1ornlem  39187  fouriersw  40211  sge0tsms  40360  sge0f1o  40362  sge0sup  40371  meadjuni  40437  ismeannd  40447  psmeasurelem  40450  psmeasure  40451  omeunile  40482  isomennd  40508  hoidmvlelem3  40574
  Copyright terms: Public domain W3C validator