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

Theorem difeq2d 3583
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 3577 . 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 1437    \ cdif 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2776  df-rab 2780  df-dif 3439
This theorem is referenced by:  difeq12d  3584  iinvdif  4371  otiunsndisj  4726  xpdifid  5284  imain  5677  dffv2  5955  f12dfv  6188  f13dfv  6189  tz7.49  7174  oev2  7237  difsnen  7664  domunsncan  7682  sbthlem2  7693  sbthlem3  7694  sbth  7702  phplem3  7763  phplem4  7764  unblem2  7834  unblem3  7835  xpfi  7852  dfac8alem  8468  dfac8a  8469  kmlem9  8596  kmlem11  8598  kmlem12  8599  compsscnvlem  8808  isercolllem3  13730  ruclem13  14294  bitsf1  14420  setsvalg  15145  setsval  15146  ismri2dad  15543  mreexmrid  15549  mreexexlemd  15550  gsumvalx  16513  gsumpropd  16515  gsumpropd2lem  16516  gsumress  16519  pmtrfv  17093  gsumval3a  17537  gsumval3  17541  dprdcntz  17640  dprddisj  17641  dprdsn  17669  dprddisj2  17672  dpjval  17689  ablfac1eu  17706  drngprop  17986  lbsind  18303  islbs2  18377  lbsextlem4  18384  lbsextg  18385  frlmlbs  19354  lindfind  19373  lindsind  19374  lindfrn  19378  f1lindf  19379  submaval  19605  mdetunilem3  19638  mdetunilem4  19639  mdetunilem9  19644  clsval2  20064  ntrval2  20065  ntrdif  20066  clsdif  20067  cmclsopn  20076  cmntrcldOLD  20078  islp  20155  pnrmopn  20358  hauscmplem  20420  bwth  20424  conndisj  20430  cvsunit  22138  bcthlem1  22291  bcth  22296  bcth3  22298  cmmbl  22487  nulmbl2  22489  shftmbl  22491  volsup  22508  mbfimaicc  22588  eldv  22852  ig1pval  23123  ig1pvalOLD  23129  tglngval  24595  axlowdimlem15  24985  axlowdim  24990  nb3graprlem2  25179  cusgrarn  25186  cusgra1v  25188  cusgra2v  25189  cusgra3v  25191  usgrasscusgra  25210  sizeusglecusglem1  25211  uvtxel  25216  cusgrauvtxb  25223  frgraunss  25722  frgra1v  25725  frgra2v  25726  frgra3v  25729  1vwmgra  25730  3vfriswmgra  25732  3cyclfrgrarn1  25739  n4cyclfrgra  25745  frgrancvvdeqlem4  25760  frgrawopreglem4  25774  frgraregorufr0  25779  2spotiundisj  25789  sigapildsyslem  28992  carsgclctunlem3  29161  sitgval  29174  ballotlemfval  29331  cvmscbv  29990  cvmsdisj  30002  cvmsss2  30006  clsun  30990  poimirlem25  31930  poimirlem26  31931  poimirlem27  31932  cnambfre  31954  watvalN  33528  dnnumch1  35873  aomclem3  35885  aomclem8  35890  nzprmdif  36639  dvmptfprodlem  37760  fouriercn  38037  carageniuncllem1  38251  nbgr2vtx1edg  39212  nbuhgr2vtx1edgb  39214  nb3grprlem2  39244  uvtxael  39249  uvtxael1  39256  uvtxusgrel  39264  cusgredg  39278  cplgr1v  39283  cplgr3v  39288  usgredgsscusgredg  39306  usgra2pthlem1  39316  lindslinindsimp2  39907  ldepsnlinc  39952
  Copyright terms: Public domain W3C validator