MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq1i Unicode version

Theorem difeq1i 3290
Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1i.1  |-  A  =  B
Assertion
Ref Expression
difeq1i  |-  ( A 
\  C )  =  ( B  \  C
)

Proof of Theorem difeq1i
StepHypRef Expression
1 difeq1i.1 . 2  |-  A  =  B
2 difeq1 3287 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2ax-mp 8 1  |-  ( A 
\  C )  =  ( B  \  C
)
Colors of variables: wff set class
Syntax hints:    = wceq 1623    \ cdif 3149
This theorem is referenced by:  difeq12i  3292  dfin3  3408  indif1  3413  indifcom  3414  difun1  3428  notab  3438  notrab  3445  undifabs  3531  orddif  4486  fresaun  5412  domunsncan  6962  phplem1  7040  elfiun  7183  axcclem  8083  dfn2  9978  restcld  16903  ufprim  17604  volun  18902  itgsplitioo  19192  ex-dif  20810  ballotlemfval0  23054  difprsn2  23191  coinflippvt  23685  wfi  24207  frind  24243  onint1  24888  bwt2  25592  nds  26150  isside0  26164  aishp  26172  kelac2  27163  islinds2  27283  lindsind2  27289  mvdco  27388  difprsng  28069  usgra0v  28117  usgra1v  28126
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator