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

Theorem difeq2d 3462
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 3456 . 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 1362    \ cdif 3313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-rab 2714  df-dif 3319
This theorem is referenced by:  difeq12d  3463  iinvdif  4230  xpdifid  5254  imain  5482  dffv2  5752  tz7.49  6886  oev2  6951  difsnen  7381  domunsncan  7399  sbthlem2  7410  sbthlem3  7411  sbth  7419  phplem3  7480  phplem4  7481  unblem2  7553  unblem3  7554  xpfi  7571  cantnffvalOLD  7859  wemapweOLD  7917  oef1oOLD  7919  dfac8alem  8187  dfac8a  8188  kmlem9  8315  kmlem11  8317  kmlem12  8318  compsscnvlem  8527  isercolllem3  13128  ruclem13  13507  bitsf1  13625  setsvalg  14180  setsval  14181  ismri2dad  14558  mreexmrid  14564  mreexexlemd  14565  gsumvalx  15484  gsumpropd  15486  gsumress  15487  pmtrfv  15938  gsumval3a  16359  gsumval3aOLD  16360  gsumval3OLD  16362  gsumval3  16365  gsumzsubmclOLD  16383  pwsgsumOLD  16448  dprdvalOLD  16461  dprdcntz  16466  dprddisj  16467  dprdsn  16507  dprddisj2  16511  dprddisj2OLD  16512  dpjval  16529  ablfac1eu  16548  drngprop  16767  lbsind  17083  islbs2  17157  lbsextlem4  17164  lbsextg  17165  frlmgsumOLD  18037  frlmlbs  18067  lindfind  18087  lindsind  18088  lindfrn  18092  f1lindf  18093  submaval  18234  mdetunilem3  18262  mdetunilem4  18263  mdetunilem9  18268  clsval2  18496  ntrval2  18497  ntrdif  18498  clsdif  18499  cmclsopn  18508  cmntrcld  18509  islp  18586  pnrmopn  18789  hauscmplem  18851  bwth  18855  conndisj  18862  cvsunit  20522  bcthlem1  20677  bcth  20682  bcth3  20684  cmmbl  20858  nulmbl2  20860  shftmbl  20862  volsup  20879  mbfimaicc  20953  eldv  21215  ig1pval  21529  tglngval  22864  axlowdimlem15  23025  axlowdim  23030  nb3graprlem2  23183  cusgrarn  23190  cusgra1v  23192  cusgra2v  23193  cusgra3v  23195  usgrasscusgra  23214  sizeusglecusglem1  23215  uvtxel  23220  cusgrauvtxb  23227  gsumpropd2lem  26093  sitgval  26566  ballotlemfval  26720  cvmscbv  26995  cvmsdisj  27007  cvmsss2  27011  cnambfre  28284  clsun  28367  dnnumch1  29242  aomclem3  29254  aomclem8  29259  mapfien2OLD  29294  otiunsndisj  29978  f12dfv  29992  f13dfv  29993  usgra2pthlem1  30146  frgraunss  30433  frgra1v  30436  frgra2v  30437  frgra3v  30440  1vwmgra  30441  3vfriswmgra  30443  3cyclfrgrarn1  30450  n4cyclfrgra  30456  frgrancvvdeqlem4  30472  frgrawopreglem4  30486  frgraregorufr0  30491  2spotiundisj  30501  lindslinindsimp2  30727  ldepsnlinc  30780  watvalN  33231
  Copyright terms: Public domain W3C validator