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

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

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 4178 . 2 (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2 df-res 5560 . 2 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
3 df-res 5560 . 2 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
41, 2, 33eqtr4g 2878 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  Vcvv 3492  cin 3932   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144  df-in 3940  df-res 5560
This theorem is referenced by:  reseq1i  5842  reseq1d  5845  imaeq1  5917  fvtresfn  6763  wfrlem1  7943  wfrlem3a  7946  wfrlem15  7958  tfrlem12  8014  pmresg  8423  resixpfo  8488  mapunen  8674  fseqenlem1  9438  axdc3lem2  9861  axdc3lem4  9863  axdc  9931  hashf1lem1  13801  lo1eq  14913  rlimeq  14914  symgfixfo  18496  lspextmo  19757  evlseu  20224  mdetunilem3  21151  mdetunilem4  21152  mdetunilem9  21157  lmbr  21794  ptuncnv  22343  iscau  23806  plyexmo  24829  relogf1o  25077  eulerpartlemt  31528  eulerpartlemgv  31530  eulerpartlemn  31538  eulerpart  31539  bnj1385  32003  bnj66  32031  bnj1234  32182  bnj1326  32195  bnj1463  32224  iscvm  32403  trpredlem1  32963  trpredtr  32966  trpredmintr  32967  frrlem1  33020  frrlem13  33032  noprefixmo  33099  nosupno  33100  nosupdm  33101  nosupfv  33103  nosupres  33104  nosupbnd1lem1  33105  nosupbnd1lem3  33107  nosupbnd1lem5  33109  nosupbnd2  33113  mbfresfi  34819  eqfnun  34878  sdclem2  34898  isdivrngo  35109  mzpcompact2lem  39226  diophrw  39234  eldioph2lem1  39235  eldioph2lem2  39236  eldioph3  39241  diophin  39247  diophrex  39250  rexrabdioph  39269  2rexfrabdioph  39271  3rexfrabdioph  39272  4rexfrabdioph  39273  6rexfrabdioph  39274  7rexfrabdioph  39275  eldioph4b  39286  pwssplit4  39567  dvnprodlem1  42107  dvnprodlem3  42109  ismea  42610  isome  42653
  Copyright terms: Public domain W3C validator