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

Theorem difeq2d 3581
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 3575 . 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 1370    \ cdif 3432
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2803  df-rab 2807  df-dif 3438
This theorem is referenced by:  difeq12d  3582  iinvdif  4349  xpdifid  5373  imain  5601  dffv2  5872  tz7.49  7009  oev2  7072  difsnen  7502  domunsncan  7520  sbthlem2  7531  sbthlem3  7532  sbth  7540  phplem3  7601  phplem4  7602  unblem2  7675  unblem3  7676  xpfi  7693  cantnffvalOLD  7981  wemapweOLD  8039  oef1oOLD  8041  dfac8alem  8309  dfac8a  8310  kmlem9  8437  kmlem11  8439  kmlem12  8440  compsscnvlem  8649  isercolllem3  13261  ruclem13  13641  bitsf1  13759  setsvalg  14314  setsval  14315  ismri2dad  14693  mreexmrid  14699  mreexexlemd  14700  gsumvalx  15620  gsumpropd  15622  gsumpropd2lem  15623  gsumress  15625  pmtrfv  16076  gsumval3a  16499  gsumval3aOLD  16500  gsumval3OLD  16502  gsumval3  16505  gsumzsubmclOLD  16523  pwsgsumOLD  16595  dprdvalOLD  16608  dprdcntz  16613  dprddisj  16614  dprdsn  16654  dprddisj2  16658  dprddisj2OLD  16659  dpjval  16676  ablfac1eu  16695  drngprop  16965  lbsind  17283  islbs2  17357  lbsextlem4  17364  lbsextg  17365  frlmgsumOLD  18319  frlmlbs  18349  lindfind  18369  lindsind  18370  lindfrn  18374  f1lindf  18375  submaval  18518  mdetunilem3  18551  mdetunilem4  18552  mdetunilem9  18557  clsval2  18785  ntrval2  18786  ntrdif  18787  clsdif  18788  cmclsopn  18797  cmntrcld  18798  islp  18875  pnrmopn  19078  hauscmplem  19140  bwth  19144  conndisj  19151  cvsunit  20811  bcthlem1  20966  bcth  20971  bcth3  20973  cmmbl  21148  nulmbl2  21150  shftmbl  21152  volsup  21169  mbfimaicc  21243  eldv  21505  ig1pval  21776  tglngval  23120  axlowdimlem15  23353  axlowdim  23358  nb3graprlem2  23511  cusgrarn  23518  cusgra1v  23520  cusgra2v  23521  cusgra3v  23523  usgrasscusgra  23542  sizeusglecusglem1  23543  uvtxel  23548  cusgrauvtxb  23555  sitgval  26861  ballotlemfval  27015  cvmscbv  27290  cvmsdisj  27302  cvmsss2  27306  cnambfre  28587  clsun  28670  dnnumch1  29544  aomclem3  29556  aomclem8  29561  mapfien2OLD  29596  otiunsndisj  30279  f12dfv  30293  f13dfv  30294  usgra2pthlem1  30447  frgraunss  30734  frgra1v  30737  frgra2v  30738  frgra3v  30741  1vwmgra  30742  3vfriswmgra  30744  3cyclfrgrarn1  30751  n4cyclfrgra  30757  frgrancvvdeqlem4  30773  frgrawopreglem4  30787  frgraregorufr0  30792  2spotiundisj  30802  lindslinindsimp2  31115  ldepsnlinc  31168  watvalN  33960
  Copyright terms: Public domain W3C validator