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

Theorem difeq2d 3622
Description: Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
difeq2d  |-  ( ph  ->  ( C  \  A
)  =  ( C 
\  B ) )

Proof of Theorem difeq2d
StepHypRef Expression
1 difeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 difeq2 3616 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C  \  A
)  =  ( C 
\  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-rab 2823  df-dif 3479
This theorem is referenced by:  difeq12d  3623  iinvdif  4397  otiunsndisj  4753  xpdifid  5433  imain  5662  dffv2  5938  f12dfv  6165  f13dfv  6166  tz7.49  7107  oev2  7170  difsnen  7596  domunsncan  7614  sbthlem2  7625  sbthlem3  7626  sbth  7634  phplem3  7695  phplem4  7696  unblem2  7769  unblem3  7770  xpfi  7787  cantnffvalOLD  8078  wemapweOLD  8136  oef1oOLD  8138  dfac8alem  8406  dfac8a  8407  kmlem9  8534  kmlem11  8536  kmlem12  8537  compsscnvlem  8746  isercolllem3  13448  ruclem13  13832  bitsf1  13951  setsvalg  14509  setsval  14510  ismri2dad  14888  mreexmrid  14894  mreexexlemd  14895  gsumvalx  15815  gsumpropd  15817  gsumpropd2lem  15818  gsumress  15820  pmtrfv  16273  gsumval3a  16696  gsumval3aOLD  16697  gsumval3OLD  16699  gsumval3  16702  gsumzsubmclOLD  16720  pwsgsumOLD  16801  dprdvalOLD  16827  dprdcntz  16832  dprddisj  16833  dprdsn  16873  dprddisj2  16877  dprddisj2OLD  16878  dpjval  16895  ablfac1eu  16914  drngprop  17190  lbsind  17509  islbs2  17583  lbsextlem4  17590  lbsextg  17591  frlmgsumOLD  18568  frlmlbs  18598  lindfind  18618  lindsind  18619  lindfrn  18623  f1lindf  18624  submaval  18850  mdetunilem3  18883  mdetunilem4  18884  mdetunilem9  18889  clsval2  19317  ntrval2  19318  ntrdif  19319  clsdif  19320  cmclsopn  19329  cmntrcld  19330  islp  19407  pnrmopn  19610  hauscmplem  19672  bwth  19676  conndisj  19683  cvsunit  21343  bcthlem1  21498  bcth  21503  bcth3  21505  cmmbl  21680  nulmbl2  21682  shftmbl  21684  volsup  21701  mbfimaicc  21775  eldv  22037  ig1pval  22308  tglngval  23666  axlowdimlem15  23935  axlowdim  23940  nb3graprlem2  24128  cusgrarn  24135  cusgra1v  24137  cusgra2v  24138  cusgra3v  24140  usgrasscusgra  24159  sizeusglecusglem1  24160  uvtxel  24165  cusgrauvtxb  24172  frgraunss  24671  frgra1v  24674  frgra2v  24675  frgra3v  24678  1vwmgra  24679  3vfriswmgra  24681  3cyclfrgrarn1  24688  n4cyclfrgra  24694  frgrancvvdeqlem4  24710  frgrawopreglem4  24724  frgraregorufr0  24729  2spotiundisj  24739  sitgval  27914  ballotlemfval  28068  cvmscbv  28343  cvmsdisj  28355  cvmsss2  28359  cnambfre  29640  clsun  29723  dnnumch1  30594  aomclem3  30606  aomclem8  30611  mapfien2OLD  30646  nzprmdif  30824  fouriercn  31533  usgra2pthlem1  31822  lindslinindsimp2  32137  ldepsnlinc  32190  watvalN  34789
  Copyright terms: Public domain W3C validator