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

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

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 3799 . 2 (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2 df-res 5116 . 2 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
3 df-res 5116 . 2 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
41, 2, 33eqtr4g 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-res 5116
This theorem is referenced by:  reseq1i  5381  reseq1d  5384  imaeq1  5449  fvtresfn  6271  wfrlem1  7399  wfrlem3a  7402  wfrlem15  7414  tfrlem12  7470  pmresg  7870  resixpfo  7931  mapunen  8114  fseqenlem1  8832  axdc3lem2  9258  axdc3lem4  9260  axdc  9328  hashf1lem1  13222  lo1eq  14280  rlimeq  14281  symgfixfo  17840  lspextmo  19037  evlseu  19497  mdetunilem3  20401  mdetunilem4  20402  mdetunilem9  20407  lmbr  21043  ptuncnv  21591  iscau  23055  plyexmo  24049  relogf1o  24294  eulerpartlemt  30407  eulerpartlemgv  30409  eulerpartlemn  30417  eulerpart  30418  bnj1385  30877  bnj66  30904  bnj1234  31055  bnj1326  31068  bnj1463  31097  iscvm  31215  trpredlem1  31701  trpredtr  31704  trpredmintr  31705  frrlem1  31754  noprefixmo  31822  nosupno  31823  nosupdm  31824  nosupfv  31826  nosupres  31827  nosupbnd1lem1  31828  nosupbnd1lem3  31830  nosupbnd1lem5  31832  nosupbnd2  31836  mbfresfi  33427  eqfnun  33487  sdclem2  33509  isdivrngo  33720  mzpcompact2lem  37133  diophrw  37141  eldioph2lem1  37142  eldioph2lem2  37143  eldioph3  37148  diophin  37155  diophrex  37158  rexrabdioph  37177  2rexfrabdioph  37179  3rexfrabdioph  37180  4rexfrabdioph  37181  6rexfrabdioph  37182  7rexfrabdioph  37183  eldioph4b  37194  pwssplit4  37478  dvnprodlem1  39924  dvnprodlem3  39926  ismea  40431  isome  40471
  Copyright terms: Public domain W3C validator