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

Theorem difeq1i 3303
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 3300 . 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 1632    \ cdif 3162
This theorem is referenced by:  difeq12i  3305  dfin3  3421  indif1  3426  indifcom  3427  difun1  3441  notab  3451  notrab  3458  undifabs  3544  difprsn1  3770  difprsn2  3771  orddif  4502  fresaun  5428  domunsncan  6978  phplem1  7056  elfiun  7199  axcclem  8099  dfn2  9994  restcld  16919  ufprim  17620  volun  18918  itgsplitioo  19208  ex-dif  20826  ballotlemfval0  23070  coinflippvt  23700  wfi  24278  frind  24314  onint1  24960  itg2addnclem  25003  bwt2  25695  nds  26253  isside0  26267  aishp  26275  kelac2  27266  islinds2  27386  lindsind2  27392  mvdco  27491  usgra0v  28251  usgra1v  28260  cusgra3v  28299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-dif 3168
  Copyright terms: Public domain W3C validator