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

Theorem difeq2d 3563
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 3557 . 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 1455    \ cdif 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-ral 2754  df-rab 2758  df-dif 3419
This theorem is referenced by:  difeq12d  3564  iinvdif  4364  otiunsndisj  4724  xpdifid  5287  imain  5685  dffv2  5966  f12dfv  6202  f13dfv  6203  tz7.49  7193  oev2  7256  difsnen  7685  domunsncan  7703  sbthlem2  7714  sbthlem3  7715  sbth  7723  phplem3  7784  phplem4  7785  unblem2  7855  unblem3  7856  xpfi  7873  dfac8alem  8491  dfac8a  8492  kmlem9  8619  kmlem11  8621  kmlem12  8622  compsscnvlem  8831  isercolllem3  13785  ruclem13  14349  bitsf1  14475  setsvalg  15200  setsval  15201  ismri2dad  15598  mreexmrid  15604  mreexexlemd  15605  gsumvalx  16568  gsumpropd  16570  gsumpropd2lem  16571  gsumress  16574  pmtrfv  17148  gsumval3a  17592  gsumval3  17596  dprdcntz  17695  dprddisj  17696  dprdsn  17724  dprddisj2  17727  dpjval  17744  ablfac1eu  17761  drngprop  18041  lbsind  18358  islbs2  18432  lbsextlem4  18439  lbsextg  18440  frlmlbs  19410  lindfind  19429  lindsind  19430  lindfrn  19434  f1lindf  19435  submaval  19661  mdetunilem3  19694  mdetunilem4  19695  mdetunilem9  19700  clsval2  20120  ntrval2  20121  ntrdif  20122  clsdif  20123  cmclsopn  20132  cmntrcldOLD  20134  islp  20211  pnrmopn  20414  hauscmplem  20476  bwth  20480  conndisj  20486  cvsunit  22194  bcthlem1  22347  bcth  22352  bcth3  22354  cmmbl  22543  nulmbl2  22545  shftmbl  22547  volsup  22565  mbfimaicc  22645  eldv  22909  ig1pval  23180  ig1pvalOLD  23186  tglngval  24652  axlowdimlem15  25042  axlowdim  25047  nb3graprlem2  25236  cusgrarn  25243  cusgra1v  25245  cusgra2v  25246  cusgra3v  25248  usgrasscusgra  25267  sizeusglecusglem1  25268  uvtxel  25273  cusgrauvtxb  25280  frgraunss  25779  frgra1v  25782  frgra2v  25783  frgra3v  25786  1vwmgra  25787  3vfriswmgra  25789  3cyclfrgrarn1  25796  n4cyclfrgra  25802  frgrancvvdeqlem4  25817  frgrawopreglem4  25831  frgraregorufr0  25836  2spotiundisj  25846  sigapildsyslem  29034  carsgclctunlem3  29202  sitgval  29215  ballotlemfval  29372  cvmscbv  30031  cvmsdisj  30043  cvmsss2  30047  clsun  31034  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  cnambfre  32035  watvalN  33604  dnnumch1  35948  aomclem3  35960  aomclem8  35965  nzprmdif  36713  dvmptfprodlem  37905  fouriercn  38197  carageniuncllem1  38450  nbgr2vtx1edg  39564  nbuhgr2vtx1edgb  39566  nb3grprlem2  39601  uvtxael  39606  uvtxael1  39614  uvtxusgrel  39622  cusgredg  39638  cplgr1v  39643  cplgr3v  39648  usgredgsscusgredg  39666  usgra2pthlem1  40036  lindslinindsimp2  40625  ldepsnlinc  40670
  Copyright terms: Public domain W3C validator