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

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

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 4164 . 2 (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2 df-res 5548 . 2 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
3 df-res 5548 . 2 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
41, 2, 33eqtr4g 2884 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  Vcvv 3479  cin 3917   × cxp 5534  cres 5538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-rab 3141  df-in 3925  df-res 5548
This theorem is referenced by:  reseq1i  5830  reseq1d  5833  imaeq1  5905  fvtresfn  6751  wfrlem1  7937  wfrlem3a  7940  wfrlem15  7952  tfrlem12  8008  pmresg  8417  resixpfo  8483  mapunen  8670  fseqenlem1  9435  axdc3lem2  9858  axdc3lem4  9860  axdc  9928  hashf1lem1  13807  lo1eq  14914  rlimeq  14915  symgfixfo  18556  lspextmo  19814  evlseu  20282  mdetunilem3  21209  mdetunilem4  21210  mdetunilem9  21215  lmbr  21852  ptuncnv  22401  iscau  23869  plyexmo  24898  relogf1o  25147  eulerpartlemt  31647  eulerpartlemgv  31649  eulerpartlemn  31657  eulerpart  31658  bnj1385  32122  bnj66  32150  bnj1234  32303  bnj1326  32316  bnj1463  32345  iscvm  32524  trpredlem1  33084  trpredtr  33087  trpredmintr  33088  frrlem1  33141  frrlem13  33153  noprefixmo  33220  nosupno  33221  nosupdm  33222  nosupfv  33224  nosupres  33225  nosupbnd1lem1  33226  nosupbnd1lem3  33228  nosupbnd1lem5  33230  nosupbnd2  33234  mbfresfi  35003  eqfnun  35060  sdclem2  35080  isdivrngo  35288  mzpcompact2lem  39524  diophrw  39532  eldioph2lem1  39533  eldioph2lem2  39534  eldioph3  39539  diophin  39545  diophrex  39548  rexrabdioph  39567  2rexfrabdioph  39569  3rexfrabdioph  39570  4rexfrabdioph  39571  6rexfrabdioph  39572  7rexfrabdioph  39573  eldioph4b  39584  pwssplit4  39865  dvnprodlem1  42430  dvnprodlem3  42432  ismea  42932  isome  42975
  Copyright terms: Public domain W3C validator