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

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

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 4169 . 2 (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2 df-res 5649 . 2 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
3 df-res 5649 . 2 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
41, 2, 33eqtr4g 2798 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  Vcvv 3447  cin 3913   × cxp 5635  cres 5639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-in 3921  df-res 5649
This theorem is referenced by:  reseq1i  5937  reseq1d  5940  imaeq1  6012  fvtresfn  6954  frrlem1  8221  frrlem13  8233  wfrlem1OLD  8258  wfrlem3OLDa  8261  wfrlem15OLD  8273  tfrlem12  8339  pmresg  8814  resixpfo  8880  mapunen  9096  fseqenlem1  9968  axdc3lem2  10395  axdc3lem4  10397  axdc  10465  hashf1lem1  14362  hashf1lem1OLD  14363  lo1eq  15459  rlimeq  15460  symgfixfo  19229  lspextmo  20561  evlseu  21516  mdetunilem3  21986  mdetunilem4  21987  mdetunilem9  21992  lmbr  22632  ptuncnv  23181  iscau  24663  plyexmo  25696  relogf1o  25945  nosupprefixmo  27071  noinfprefixmo  27072  nosupcbv  27073  nosupno  27074  nosupdm  27075  nosupfv  27077  nosupres  27078  nosupbnd1lem1  27079  nosupbnd1lem3  27081  nosupbnd1lem5  27083  nosupbnd2  27087  noinfcbv  27088  noinfno  27089  noinfdm  27090  noinffv  27092  noinfres  27093  noinfbnd1lem1  27094  noinfbnd1lem3  27096  noinfbnd1lem5  27098  noinfbnd2  27102  eulerpartlemt  33035  eulerpartlemgv  33037  eulerpartlemn  33045  eulerpart  33046  bnj1385  33508  bnj66  33536  bnj1234  33689  bnj1326  33702  bnj1463  33731  iscvm  33917  mbfresfi  36174  eqfnun  36231  sdclem2  36251  isdivrngo  36459  mzpcompact2lem  41121  diophrw  41129  eldioph2lem1  41130  eldioph2lem2  41131  eldioph3  41136  diophin  41142  diophrex  41145  rexrabdioph  41164  2rexfrabdioph  41166  3rexfrabdioph  41167  4rexfrabdioph  41168  6rexfrabdioph  41169  7rexfrabdioph  41170  eldioph4b  41181  pwssplit4  41463  dvnprodlem1  44277  dvnprodlem3  44279  ismea  44782  isome  44825
  Copyright terms: Public domain W3C validator