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

Theorem difeq1d 3424
Description: Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
difeq1d  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )

Proof of Theorem difeq1d
StepHypRef Expression
1 difeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 difeq1 3418 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    \ cdif 3277
This theorem is referenced by:  difeq12d  3426  diftpsn3  3897  dffv2  5755  phplem4  7248  unfilem3  7332  marypha1lem  7396  infdifsn  7567  cantnfp1lem3  7592  isacn  7881  cda1dif  8012  fin23lem28  8176  enfin1ai  8220  fin1a2lem7  8242  axdc4uz  11277  leiso  11663  isstruct2  13433  strle1  13515  pltfval  14371  gsumval3  15469  dmdprd  15514  dprd2da  15555  dmdprdsplit2lem  15558  dpjfval  15568  ablfac1eulem  15585  lssset  15965  lbspropd  16126  opsrtoslem2  16500  cldval  17042  difopn  17053  mretopd  17111  restcld  17190  ordtcld1  17215  ordtcld2  17216  cnclima  17286  iscncl  17287  isreg2  17395  llycmpkgen2  17535  1stckgen  17539  ptval  17555  txcld  17588  ptcld  17598  txkgen  17637  qtopcld  17698  qtoprest  17702  qtopcmap  17704  kqcldsat  17718  regr1lem  17724  trufil  17895  ufildr  17916  opnsubg  18090  cldsubg  18093  blcld  18488  lebnumlem1  18939  bcthlem1  19230  bcth  19235  bcth3  19237  difmbl  19390  itg1val  19528  itgioo  19660  limciun  19734  dvfval  19737  isuhgra  21291  uhgraeq12d  21295  isumgra  21303  isuslgra  21325  isusgra  21326  usgraeq12d  21338  nb3graprlem2  21414  cusgra3v  21426  isconngra1  21613  imadifxp  23991  gtiso  24041  difico  24099  imambfm  24565  issibf  24601  sibf0  24602  sitgfval  24608  ballotlemfval  24700  ballotlemfp1  24702  ballotlemgun  24735  kur14  24855  iscvm  24899  cvmscld  24913  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem  26155  itg2addnclem2  26156  topbnd  26217  aomclem8  27027  kelac2  27031  islindf  27150  islindf2  27152  f1lindf  27160  en2other2  27250  f1omvdco2  27259  symgsssg  27276  symgfisg  27277  symggen  27279  psgnunilem1  27284  psgnunilem5  27285  psgnunilem2  27286  psgnunilem3  27287  frgra3v  28106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-dif 3283
  Copyright terms: Public domain W3C validator