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

Theorem difeq2d 3589
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 3583 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2syl 17 1  |-  ( ph  ->  ( C  \  A
)  =  ( C 
\  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    \ cdif 3439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2787  df-rab 2791  df-dif 3445
This theorem is referenced by:  difeq12d  3590  iinvdif  4374  otiunsndisj  4727  xpdifid  5285  imain  5677  dffv2  5954  f12dfv  6187  f13dfv  6188  tz7.49  7170  oev2  7233  difsnen  7660  domunsncan  7678  sbthlem2  7689  sbthlem3  7690  sbth  7698  phplem3  7759  phplem4  7760  unblem2  7830  unblem3  7831  xpfi  7848  dfac8alem  8458  dfac8a  8459  kmlem9  8586  kmlem11  8588  kmlem12  8589  compsscnvlem  8798  isercolllem3  13708  ruclem13  14272  bitsf1  14394  setsvalg  15108  setsval  15109  ismri2dad  15494  mreexmrid  15500  mreexexlemd  15501  gsumvalx  16464  gsumpropd  16466  gsumpropd2lem  16467  gsumress  16470  pmtrfv  17044  gsumval3a  17472  gsumval3  17476  dprdcntz  17575  dprddisj  17576  dprdsn  17604  dprddisj2  17607  dpjval  17624  ablfac1eu  17641  drngprop  17921  lbsind  18238  islbs2  18312  lbsextlem4  18319  lbsextg  18320  frlmlbs  19286  lindfind  19305  lindsind  19306  lindfrn  19310  f1lindf  19311  submaval  19537  mdetunilem3  19570  mdetunilem4  19571  mdetunilem9  19576  clsval2  19996  ntrval2  19997  ntrdif  19998  clsdif  19999  cmclsopn  20008  cmntrcldOLD  20010  islp  20087  pnrmopn  20290  hauscmplem  20352  bwth  20356  conndisj  20362  cvsunit  22032  bcthlem1  22185  bcth  22190  bcth3  22192  cmmbl  22365  nulmbl2  22367  shftmbl  22369  volsup  22386  mbfimaicc  22466  eldv  22730  ig1pval  22998  tglngval  24456  axlowdimlem15  24832  axlowdim  24837  nb3graprlem2  25025  cusgrarn  25032  cusgra1v  25034  cusgra2v  25035  cusgra3v  25037  usgrasscusgra  25056  sizeusglecusglem1  25057  uvtxel  25062  cusgrauvtxb  25069  frgraunss  25568  frgra1v  25571  frgra2v  25572  frgra3v  25575  1vwmgra  25576  3vfriswmgra  25578  3cyclfrgrarn1  25585  n4cyclfrgra  25591  frgrancvvdeqlem4  25606  frgrawopreglem4  25620  frgraregorufr0  25625  2spotiundisj  25635  sigapildsyslem  28822  carsgclctunlem3  28981  sitgval  28993  ballotlemfval  29148  cvmscbv  29769  cvmsdisj  29781  cvmsss2  29785  clsun  30769  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  cnambfre  31693  watvalN  33267  dnnumch1  35608  aomclem3  35620  aomclem8  35625  nzprmdif  36305  dvmptfprodlem  37388  fouriercn  37664  carageniuncllem1  37851  usgra2pthlem1  38423  lindslinindsimp2  39016  ldepsnlinc  39061
  Copyright terms: Public domain W3C validator