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

Theorem difeq2d 3618
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 3612 . 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 1395    \ cdif 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-rab 2816  df-dif 3474
This theorem is referenced by:  difeq12d  3619  iinvdif  4404  otiunsndisj  4762  xpdifid  5442  imain  5670  dffv2  5946  f12dfv  6180  f13dfv  6181  tz7.49  7128  oev2  7191  difsnen  7618  domunsncan  7636  sbthlem2  7647  sbthlem3  7648  sbth  7656  phplem3  7717  phplem4  7718  unblem2  7791  unblem3  7792  xpfi  7809  cantnffvalOLD  8099  wemapweOLD  8157  oef1oOLD  8159  dfac8alem  8427  dfac8a  8428  kmlem9  8555  kmlem11  8557  kmlem12  8558  compsscnvlem  8767  isercolllem3  13500  ruclem13  13986  bitsf1  14107  setsvalg  14667  setsval  14668  ismri2dad  15053  mreexmrid  15059  mreexexlemd  15060  gsumvalx  16023  gsumpropd  16025  gsumpropd2lem  16026  gsumress  16029  pmtrfv  16603  gsumval3a  17031  gsumval3aOLD  17032  gsumval3OLD  17034  gsumval3  17037  gsumzsubmclOLD  17055  pwsgsumOLD  17136  dprdvalOLD  17162  dprdcntz  17167  dprddisj  17168  dprdsn  17209  dprddisj2  17213  dprddisj2OLD  17214  dpjval  17231  ablfac1eu  17250  drngprop  17533  lbsind  17852  islbs2  17926  lbsextlem4  17933  lbsextg  17934  frlmgsumOLD  18927  frlmlbs  18957  lindfind  18977  lindsind  18978  lindfrn  18982  f1lindf  18983  submaval  19209  mdetunilem3  19242  mdetunilem4  19243  mdetunilem9  19248  clsval2  19677  ntrval2  19678  ntrdif  19679  clsdif  19680  cmclsopn  19689  cmntrcld  19690  islp  19767  pnrmopn  19970  hauscmplem  20032  bwth  20036  conndisj  20042  cvsunit  21733  bcthlem1  21888  bcth  21893  bcth3  21895  cmmbl  22070  nulmbl2  22072  shftmbl  22074  volsup  22091  mbfimaicc  22165  eldv  22427  ig1pval  22698  tglngval  24063  ishpg  24253  axlowdimlem15  24385  axlowdim  24390  nb3graprlem2  24578  cusgrarn  24585  cusgra1v  24587  cusgra2v  24588  cusgra3v  24590  usgrasscusgra  24609  sizeusglecusglem1  24610  uvtxel  24615  cusgrauvtxb  24622  frgraunss  25121  frgra1v  25124  frgra2v  25125  frgra3v  25128  1vwmgra  25129  3vfriswmgra  25131  3cyclfrgrarn1  25138  n4cyclfrgra  25144  frgrancvvdeqlem4  25159  frgrawopreglem4  25173  frgraregorufr0  25178  2spotiundisj  25188  sitgval  28449  ballotlemfval  28603  cvmscbv  28878  cvmsdisj  28890  cvmsss2  28894  cnambfre  30225  clsun  30308  dnnumch1  31152  aomclem3  31164  aomclem8  31169  mapfien2OLD  31204  nzprmdif  31386  dvmptfprodlem  31902  fouriercn  32176  usgra2pthlem1  32573  lindslinindsimp2  33166  ldepsnlinc  33211  watvalN  35818
  Copyright terms: Public domain W3C validator