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

Theorem difeq2d 3307
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 3301 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2syl 15 1  |-  ( ph  ->  ( C  \  A
)  =  ( C 
\  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    \ cdif 3162
This theorem is referenced by:  difeq12d  3308  imain  5344  dffv2  5608  tz7.49  6473  oev2  6538  difsnen  6960  domunsncan  6978  sbthlem2  6988  sbthlem3  6989  sbth  6997  phplem3  7058  phplem4  7059  unblem2  7126  unblem3  7127  xpfi  7144  wemapwe  7416  oef1o  7417  dfac8alem  7672  dfac8a  7673  kmlem9  7800  kmlem11  7802  kmlem12  7803  compsscnvlem  8012  isercolllem3  12156  ruclem13  12536  bitsf1  12653  setsvalg  13187  setsval  13188  ismri2dad  13555  mreexmrid  13561  mreexexlemd  13562  gsumvalx  14467  gsumpropd  14469  gsumress  14470  gsumval3a  15205  gsumval3  15207  gsumzsubmcl  15216  pwsgsum  15246  dprdval  15254  dprdcntz  15259  dprddisj  15260  dprdsn  15287  dprddisj2  15290  dpjval  15307  ablfac1eu  15324  drngprop  15539  lbsind  15849  islbs2  15923  lbsextlem4  15930  lbsextg  15931  mplval  16189  ressmplbas2  16215  mplbaspropd  16330  clsval2  16803  ntrval2  16804  ntrdif  16805  clsdif  16806  cmclsopn  16815  cmntrcld  16816  islp  16888  pnrmopn  17087  hauscmplem  17149  conndisj  17158  bcthlem1  18762  bcth  18767  bcth3  18769  cmmbl  18908  nulmbl2  18910  shftmbl  18912  volsup  18929  mbfimaicc  19004  eldv  19264  mdegfval  19464  mdegpropd  19486  ig1pval  19574  ballotlemfval  23064  gsumpropd2lem  23394  cvmscbv  23804  cvmsdisj  23816  cvmsss2  23820  axlowdimlem15  24656  axlowdim  24661  isder  25810  clsun  26349  dnnumch1  27244  aomclem3  27256  aomclem8  27262  frlmgsum  27335  uvcresum  27345  frlmlbs  27352  frlmup1  27353  mapfien2  27361  lindfind  27389  lindsind  27390  lindfrn  27394  f1lindf  27395  pmtrfv  27498  nb3graprlem2  28288  cusgra1v  28296  cusgra2v  28297  cusgra3v  28299  uvtxel  28302  uvtxisvtx  28303  cusgrauvtx  28309  frgra1v  28422  frgra2v  28423  frgra3v  28426  1vwmgra  28427  3vfriswmgra  28429  3cyclfrgrarn1  28435  n4cyclfrgra  28440  watvalN  30804
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-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-rab 2565  df-dif 3168
  Copyright terms: Public domain W3C validator