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

Theorem difeq2d 3294
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 3288 . 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 1623    \ cdif 3149
This theorem is referenced by:  difeq12d  3295  imain  5328  dffv2  5592  tz7.49  6457  oev2  6522  difsnen  6944  domunsncan  6962  sbthlem2  6972  sbthlem3  6973  sbth  6981  phplem3  7042  phplem4  7043  unblem2  7110  unblem3  7111  xpfi  7128  wemapwe  7400  oef1o  7401  dfac8alem  7656  dfac8a  7657  kmlem9  7784  kmlem11  7786  kmlem12  7787  compsscnvlem  7996  isercolllem3  12140  ruclem13  12520  bitsf1  12637  setsvalg  13171  setsval  13172  ismri2dad  13539  mreexmrid  13545  mreexexlemd  13546  gsumvalx  14451  gsumpropd  14453  gsumress  14454  gsumval3a  15189  gsumval3  15191  gsumzsubmcl  15200  pwsgsum  15230  dprdval  15238  dprdcntz  15243  dprddisj  15244  dprdsn  15271  dprddisj2  15274  dpjval  15291  ablfac1eu  15308  drngprop  15523  lbsind  15833  islbs2  15907  lbsextlem4  15914  lbsextg  15915  mplval  16173  ressmplbas2  16199  mplbaspropd  16314  clsval2  16787  ntrval2  16788  ntrdif  16789  clsdif  16790  cmclsopn  16799  cmntrcld  16800  islp  16872  pnrmopn  17071  hauscmplem  17133  conndisj  17142  bcthlem1  18746  bcth  18751  bcth3  18753  cmmbl  18892  nulmbl2  18894  shftmbl  18896  volsup  18913  mbfimaicc  18988  eldv  19248  mdegfval  19448  mdegpropd  19470  ig1pval  19558  ballotlemfval  23048  gsumpropd2lem  23379  cvmscbv  23789  cvmsdisj  23801  cvmsss2  23805  axlowdimlem15  24584  axlowdim  24589  isder  25707  clsun  26246  dnnumch1  27141  aomclem3  27153  aomclem8  27159  frlmgsum  27232  uvcresum  27242  frlmlbs  27249  frlmup1  27250  mapfien2  27258  lindfind  27286  lindsind  27287  lindfrn  27291  f1lindf  27292  pmtrfv  27395  cusgra1v  28157  cusgra2v  28158  uvtxel  28161  uvtxisvtx  28162  cusgrauvtx  28168  frgra1v  28176  frgra2v  28177  frgra3v  28180  1vwmgra  28181  3vfriswmgra  28183  watvalN  30182
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-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator