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

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

Proof of Theorem reseq1
StepHypRef Expression
1 ineq1 3840 . 2 (𝐴 = 𝐵 → (𝐴 ∩ (𝐶 × V)) = (𝐵 ∩ (𝐶 × V)))
2 df-res 5155 . 2 (𝐴𝐶) = (𝐴 ∩ (𝐶 × V))
3 df-res 5155 . 2 (𝐵𝐶) = (𝐵 ∩ (𝐶 × V))
41, 2, 33eqtr4g 2710 1 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  Vcvv 3231  cin 3606   × cxp 5141  cres 5145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-res 5155
This theorem is referenced by:  reseq1i  5424  reseq1d  5427  imaeq1  5496  fvtresfn  6323  wfrlem1  7459  wfrlem3a  7462  wfrlem15  7474  tfrlem12  7530  pmresg  7927  resixpfo  7988  mapunen  8170  fseqenlem1  8885  axdc3lem2  9311  axdc3lem4  9313  axdc  9381  hashf1lem1  13277  lo1eq  14343  rlimeq  14344  symgfixfo  17905  lspextmo  19104  evlseu  19564  mdetunilem3  20468  mdetunilem4  20469  mdetunilem9  20474  lmbr  21110  ptuncnv  21658  iscau  23120  plyexmo  24113  relogf1o  24358  eulerpartlemt  30561  eulerpartlemgv  30563  eulerpartlemn  30571  eulerpart  30572  bnj1385  31029  bnj66  31056  bnj1234  31207  bnj1326  31220  bnj1463  31249  iscvm  31367  trpredlem1  31851  trpredtr  31854  trpredmintr  31855  frrlem1  31905  noprefixmo  31973  nosupno  31974  nosupdm  31975  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd2  31987  mbfresfi  33586  eqfnun  33646  sdclem2  33668  isdivrngo  33879  mzpcompact2lem  37631  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  eldioph3  37646  diophin  37653  diophrex  37656  rexrabdioph  37675  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  eldioph4b  37692  pwssplit4  37976  dvnprodlem1  40479  dvnprodlem3  40481  ismea  40986  isome  41029
  Copyright terms: Public domain W3C validator