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

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

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 3764 . 2 (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2 df-res 5036 . 2 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
3 df-res 5036 . 2 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
41, 2, 33eqtr4g 2664 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  Vcvv 3168  cin 3534   × cxp 5022  cres 5026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-in 3542  df-res 5036
This theorem is referenced by:  reseq1i  5296  reseq1d  5299  imaeq1  5363  fvtresfn  6174  wfrlem1  7274  wfrlem3a  7277  wfrlem15  7289  tfrlem12  7345  pmresg  7744  resixpfo  7805  mapunen  7987  fseqenlem1  8703  axdc3lem2  9129  axdc3lem4  9131  axdc  9199  hashf1lem1  13044  lo1eq  14089  rlimeq  14090  symgfixfo  17624  lspextmo  18819  evlseu  19279  mdetunilem3  20177  mdetunilem4  20178  mdetunilem9  20183  lmbr  20810  ptuncnv  21358  iscau  22796  plyexmo  23785  relogf1o  24030  eulerpartlemt  29562  eulerpartlemgv  29564  eulerpartlemn  29572  eulerpart  29573  bnj1385  29959  bnj66  29986  bnj1234  30137  bnj1326  30150  bnj1463  30179  iscvm  30297  trpredlem1  30773  trpredtr  30776  trpredmintr  30777  frrlem1  30826  nofulllem5  30907  mbfresfi  32425  eqfnun  32485  sdclem2  32507  isdivrngo  32718  mzpcompact2lem  36131  diophrw  36139  eldioph2lem1  36140  eldioph2lem2  36141  eldioph3  36146  diophin  36153  diophrex  36156  rexrabdioph  36175  2rexfrabdioph  36177  3rexfrabdioph  36178  4rexfrabdioph  36179  6rexfrabdioph  36180  7rexfrabdioph  36181  eldioph4b  36192  pwssplit4  36476  dvnprodlem1  38636  dvnprodlem3  38638  ismea  39144  isome  39184
  Copyright terms: Public domain W3C validator