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

Theorem difeq1d 3621
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 3615 . 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 1379    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-dif 3479
This theorem is referenced by:  difeq12d  3623  diftpsn3  4165  dffv2  5938  phplem4  7696  unfilem3  7782  marypha1lem  7889  infdifsn  8069  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  en2other2  8383  isacn  8421  cda1dif  8552  fin23lem28  8716  enfin1ai  8760  fin1a2lem7  8782  fzdifsuc  11735  axdc4uz  12057  leiso  12470  isstruct2  14495  strle1  14582  pltfval  15442  f1omvdco2  16269  symgsssg  16288  symgfisg  16289  symggen  16291  pmtrdifellem3  16299  pmtrdifwrdellem3  16304  pmtrdifwrdel2lem1  16305  pmtrdifwrdel  16306  pmtrdifwrdel2  16307  psgnunilem1  16314  psgnunilem5  16315  psgnunilem2  16316  psgnunilem3  16317  gsumval3OLD  16699  gsumval3  16702  dmdprd  16820  dprd2da  16881  dmdprdsplit2lem  16884  dpjfval  16894  ablfac1eulem  16913  lssset  17363  lbspropd  17528  opsrtoslem2  17920  islindf  18614  islindf2  18616  f1lindf  18624  cldval  19290  difopn  19301  mretopd  19359  restcld  19439  ordtcld1  19464  ordtcld2  19465  cnclima  19535  iscncl  19536  isreg2  19644  llycmpkgen2  19786  1stckgen  19790  ptval  19806  txcld  19839  ptcld  19849  txkgen  19888  qtopcld  19949  qtoprest  19953  qtopcmap  19955  kqcldsat  19969  regr1lem  19975  trufil  20146  ufildr  20167  opnsubg  20341  cldsubg  20344  blcld  20743  lebnumlem1  21196  bcthlem1  21498  bcth  21503  bcth3  21505  difmbl  21688  itg1val  21825  itgioo  21957  limciun  22033  dvfval  22036  istrkgl  23583  eengv  23958  elntg  23963  isuhgra  23974  isushgra  23977  uhgrac  23981  uhgraeq12d  23983  isumgra  23991  isuslgra  24019  isusgra  24020  usgraeq12d  24038  nb3graprlem2  24128  cusgra3v  24140  isconngra1  24349  frgra3v  24678  imadifxp  27131  gtiso  27191  difico  27262  submarchi  27392  qtophaus  27637  imambfm  27873  issibf  27915  sibf0  27916  sitgfval  27923  ballotlemfval  28068  ballotlemfp1  28070  ballotlemgun  28103  kur14  28300  iscvm  28344  cvmscld  28358  mblfinlem3  29630  mblfinlem4  29631  itg2addnclem  29643  itg2addnclem2  29644  topbnd  29719  aomclem8  30611  kelac2  30615  iccdifioo  31119  iccdifprioo  31120  ibliooicc  31289  dirkercncflem2  31404  isuhgr  31835  isushgr  31836  uhgeq12g  31839  uhguhgra  31841  uhgrauhg  31842  uhg0v  31846  uhgun  31849
  Copyright terms: Public domain W3C validator