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

Theorem difeq1d 3470
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 3464 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    \ cdif 3322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-dif 3328
This theorem is referenced by:  difeq12d  3472  diftpsn3  4009  dffv2  5761  phplem4  7489  unfilem3  7574  marypha1lem  7679  infdifsn  7858  cantnfp1lem3  7884  cantnfp1lem3OLD  7910  en2other2  8172  isacn  8210  cda1dif  8341  fin23lem28  8505  enfin1ai  8549  fin1a2lem7  8571  fzdifsuc  11512  axdc4uz  11801  leiso  12208  isstruct2  14179  strle1  14265  pltfval  15125  f1omvdco2  15947  symgsssg  15966  symgfisg  15967  symggen  15969  pmtrdifellem3  15977  pmtrdifwrdellem3  15982  pmtrdifwrdel2lem1  15983  pmtrdifwrdel  15984  pmtrdifwrdel2  15985  psgnunilem1  15992  psgnunilem5  15993  psgnunilem2  15994  psgnunilem3  15995  gsumval3OLD  16375  gsumval3  16378  dmdprd  16470  dprd2da  16531  dmdprdsplit2lem  16534  dpjfval  16544  ablfac1eulem  16563  lssset  16993  lbspropd  17158  opsrtoslem2  17542  islindf  18200  islindf2  18202  f1lindf  18210  cldval  18586  difopn  18597  mretopd  18655  restcld  18735  ordtcld1  18760  ordtcld2  18761  cnclima  18831  iscncl  18832  isreg2  18940  llycmpkgen2  19082  1stckgen  19086  ptval  19102  txcld  19135  ptcld  19145  txkgen  19184  qtopcld  19245  qtoprest  19249  qtopcmap  19251  kqcldsat  19265  regr1lem  19271  trufil  19442  ufildr  19463  opnsubg  19637  cldsubg  19640  blcld  20039  lebnumlem1  20492  bcthlem1  20794  bcth  20799  bcth3  20801  difmbl  20983  itg1val  21120  itgioo  21252  limciun  21328  dvfval  21331  istrkgl  22880  eengv  23160  elntg  23165  isuhgra  23172  uhgraeq12d  23176  isumgra  23184  isuslgra  23206  isusgra  23207  usgraeq12d  23219  nb3graprlem2  23295  cusgra3v  23307  isconngra1  23494  imadifxp  25874  gtiso  25931  difico  26006  submarchi  26136  imambfm  26613  issibf  26649  sibf0  26650  sitgfval  26657  ballotlemfval  26802  ballotlemfp1  26804  ballotlemgun  26837  kur14  27034  iscvm  27078  cvmscld  27092  mblfinlem3  28355  mblfinlem4  28356  itg2addnclem  28368  itg2addnclem2  28369  topbnd  28444  aomclem8  29339  kelac2  29343  frgra3v  30519
  Copyright terms: Public domain W3C validator