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

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

Proof of Theorem reseq2
StepHypRef Expression
1 xpeq1 5568 . . 3 (𝐴 = 𝐵 → (𝐴 × V) = (𝐵 × V))
21ineq2d 4193 . 2 (𝐴 = 𝐵 → (𝐶 ∩ (𝐴 × V)) = (𝐶 ∩ (𝐵 × V)))
3 df-res 5566 . 2 (𝐶𝐴) = (𝐶 ∩ (𝐴 × V))
4 df-res 5566 . 2 (𝐶𝐵) = (𝐶 ∩ (𝐵 × V))
52, 3, 43eqtr4g 2886 1 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  Vcvv 3500  cin 3939   × cxp 5552  cres 5556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-rab 3152  df-in 3947  df-opab 5126  df-xp 5560  df-res 5566
This theorem is referenced by:  reseq2i  5849  reseq2d  5852  resabs1  5882  resima2  5887  imaeq2  5924  resdisj  6025  fimadmfoALT  6600  fressnfv  6920  tfrlem1  8008  tfrlem9  8017  tfrlem11  8020  tfrlem12  8021  tfr2b  8028  tz7.44-1  8038  tz7.44-2  8039  tz7.44-3  8040  rdglem1  8047  fnfi  8790  fseqenlem1  9444  rtrclreclem4  14415  psgnprfval1  18586  gsumzaddlem  18977  gsum2dlem2  19027  znunithash  20646  islinds  20888  lmbr2  21802  lmff  21844  kgencn2  22100  ptcmpfi  22356  tsmsgsum  22681  tsmsres  22686  tsmsf1o  22687  tsmsxplem1  22695  tsmsxp  22697  ustval  22745  xrge0gsumle  23375  xrge0tsms  23376  lmmbr2  23796  lmcau  23850  limcun  24427  jensen  25499  wilthlem2  25579  wilthlem3  25580  hhssnvt  28975  hhsssh  28979  foresf1o  30198  reldisjun  30287  xrge0tsmsd  30625  gsumle  30658  esumsnf  31228  subfacp1lem3  32332  subfacp1lem5  32334  erdszelem1  32341  erdsze  32352  erdsze2lem2  32354  cvmscbv  32408  cvmshmeo  32421  cvmsss2  32424  dfpo2  32894  eldm3  32900  dfrdg2  32943  bj-diagval  34364  mbfresfi  34824  elcoeleqvrels  35716  eleldisjs  35847  eldisjeq  35860  mzpcompact2lem  39232  seff  40525  wessf1ornlem  41329  fouriersw  42401  sge0tsms  42547  sge0f1o  42549  sge0sup  42558  meadjuni  42624  ismeannd  42634  psmeasurelem  42637  psmeasure  42638  omeunile  42672  isomennd  42698  hoidmvlelem3  42764
  Copyright terms: Public domain W3C validator