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

Theorem difeq2d 3469
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 3463 . 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 1369    \ cdif 3320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2715  df-rab 2719  df-dif 3326
This theorem is referenced by:  difeq12d  3470  iinvdif  4237  xpdifid  5261  imain  5489  dffv2  5759  tz7.49  6892  oev2  6955  difsnen  7385  domunsncan  7403  sbthlem2  7414  sbthlem3  7415  sbth  7423  phplem3  7484  phplem4  7485  unblem2  7557  unblem3  7558  xpfi  7575  cantnffvalOLD  7863  wemapweOLD  7921  oef1oOLD  7923  dfac8alem  8191  dfac8a  8192  kmlem9  8319  kmlem11  8321  kmlem12  8322  compsscnvlem  8531  isercolllem3  13136  ruclem13  13516  bitsf1  13634  setsvalg  14189  setsval  14190  ismri2dad  14567  mreexmrid  14573  mreexexlemd  14574  gsumvalx  15493  gsumpropd  15495  gsumpropd2lem  15496  gsumress  15498  pmtrfv  15949  gsumval3a  16370  gsumval3aOLD  16371  gsumval3OLD  16373  gsumval3  16376  gsumzsubmclOLD  16394  pwsgsumOLD  16462  dprdvalOLD  16475  dprdcntz  16480  dprddisj  16481  dprdsn  16521  dprddisj2  16525  dprddisj2OLD  16526  dpjval  16543  ablfac1eu  16562  drngprop  16821  lbsind  17138  islbs2  17212  lbsextlem4  17219  lbsextg  17220  frlmgsumOLD  18170  frlmlbs  18200  lindfind  18220  lindsind  18221  lindfrn  18225  f1lindf  18226  submaval  18367  mdetunilem3  18395  mdetunilem4  18396  mdetunilem9  18401  clsval2  18629  ntrval2  18630  ntrdif  18631  clsdif  18632  cmclsopn  18641  cmntrcld  18642  islp  18719  pnrmopn  18922  hauscmplem  18984  bwth  18988  conndisj  18995  cvsunit  20655  bcthlem1  20810  bcth  20815  bcth3  20817  cmmbl  20991  nulmbl2  20993  shftmbl  20995  volsup  21012  mbfimaicc  21086  eldv  21348  ig1pval  21619  tglngval  22959  axlowdimlem15  23153  axlowdim  23158  nb3graprlem2  23311  cusgrarn  23318  cusgra1v  23320  cusgra2v  23321  cusgra3v  23323  usgrasscusgra  23342  sizeusglecusglem1  23343  uvtxel  23348  cusgrauvtxb  23355  sitgval  26670  ballotlemfval  26824  cvmscbv  27099  cvmsdisj  27111  cvmsss2  27115  cnambfre  28393  clsun  28476  dnnumch1  29350  aomclem3  29362  aomclem8  29367  mapfien2OLD  29402  otiunsndisj  30085  f12dfv  30099  f13dfv  30100  usgra2pthlem1  30253  frgraunss  30540  frgra1v  30543  frgra2v  30544  frgra3v  30547  1vwmgra  30548  3vfriswmgra  30550  3cyclfrgrarn1  30557  n4cyclfrgra  30563  frgrancvvdeqlem4  30579  frgrawopreglem4  30593  frgraregorufr0  30598  2spotiundisj  30608  lindslinindsimp2  30886  ldepsnlinc  30939  watvalN  33477
  Copyright terms: Public domain W3C validator