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

Theorem difeq2d 3467
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 3461 . 2  |-  ( A  =  B  ->  ( C  \  A )  =  ( C  \  B
) )
31, 2syl 16 1  |-  ( ph  ->  ( C  \  A
)  =  ( C 
\  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    \ cdif 3319
This theorem is referenced by:  difeq12d  3468  imain  5531  dffv2  5798  tz7.49  6704  oev2  6769  difsnen  7192  domunsncan  7210  sbthlem2  7220  sbthlem3  7221  sbth  7229  phplem3  7290  phplem4  7291  unblem2  7362  unblem3  7363  xpfi  7380  wemapwe  7656  oef1o  7657  dfac8alem  7912  dfac8a  7913  kmlem9  8040  kmlem11  8042  kmlem12  8043  compsscnvlem  8252  isercolllem3  12462  ruclem13  12843  bitsf1  12960  setsvalg  13494  setsval  13495  ismri2dad  13864  mreexmrid  13870  mreexexlemd  13871  gsumvalx  14776  gsumpropd  14778  gsumress  14779  gsumval3a  15514  gsumval3  15516  gsumzsubmcl  15525  pwsgsum  15555  dprdval  15563  dprdcntz  15568  dprddisj  15569  dprdsn  15596  dprddisj2  15599  dpjval  15616  ablfac1eu  15633  drngprop  15848  lbsind  16154  islbs2  16228  lbsextlem4  16235  lbsextg  16236  mplval  16494  ressmplbas2  16520  mplbaspropd  16632  clsval2  17116  ntrval2  17117  ntrdif  17118  clsdif  17119  cmclsopn  17128  cmntrcld  17129  islp  17206  pnrmopn  17409  hauscmplem  17471  conndisj  17481  bcthlem1  19279  bcth  19284  bcth3  19286  cmmbl  19431  nulmbl2  19433  shftmbl  19435  volsup  19452  mbfimaicc  19527  eldv  19787  mdegfval  19987  mdegpropd  20009  ig1pval  20097  nb3graprlem2  21463  cusgrarn  21470  cusgra1v  21472  cusgra2v  21473  cusgra3v  21475  usgrasscusgra  21494  sizeusglecusglem1  21495  uvtxel  21500  cusgrauvtxb  21507  gsumpropd2lem  24222  sitgval  24649  ballotlemfval  24749  cvmscbv  24947  cvmsdisj  24959  cvmsss2  24963  axlowdimlem15  25897  axlowdim  25902  cnambfre  26257  clsun  26333  dnnumch1  27121  aomclem3  27133  aomclem8  27138  frlmgsum  27211  uvcresum  27221  frlmlbs  27228  frlmup1  27229  mapfien2  27237  lindfind  27265  lindsind  27266  lindfrn  27270  f1lindf  27271  pmtrfv  27374  otiunsndisj  28069  f12dfv  28086  f13dfv  28087  usgra2pthlem1  28336  frgraunss  28447  frgra1v  28450  frgra2v  28451  frgra3v  28454  1vwmgra  28455  3vfriswmgra  28457  3cyclfrgrarn1  28464  n4cyclfrgra  28470  frgrancvvdeqlem4  28484  frgrawopreglem4  28498  frgraregorufr0  28503  2spotiundisj  28513  watvalN  30852
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-rab 2716  df-dif 3325
  Copyright terms: Public domain W3C validator