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

Theorem difeq1d 3559
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 3553 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2syl 17 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    \ cdif 3410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-dif 3416
This theorem is referenced by:  difeq12d  3561  diftpsn3  4109  dffv2  5921  phplem4  7736  unfilem3  7819  marypha1lem  7926  infdifsn  8105  cantnfp1lem3  8130  cantnfp1lem3OLD  8156  en2other2  8418  isacn  8456  cda1dif  8587  fin23lem28  8751  enfin1ai  8795  fin1a2lem7  8817  fzdifsuc  11792  axdc4uz  12132  leiso  12555  isstruct2  14848  strle1  14938  pltfval  15911  f1omvdco2  16795  symgsssg  16814  symgfisg  16815  symggen  16817  pmtrdifellem3  16825  pmtrdifwrdellem3  16830  pmtrdifwrdel2lem1  16831  pmtrdifwrdel  16832  pmtrdifwrdel2  16833  psgnunilem1  16840  psgnunilem5  16841  psgnunilem2  16842  psgnunilem3  16843  gsumval3OLD  17230  gsumval3  17233  dmdprd  17347  dprd2da  17409  dmdprdsplit2lem  17412  dpjfval  17422  ablfac1eulem  17441  lssset  17898  lbspropd  18063  opsrtoslem2  18467  islindf  19137  islindf2  19139  f1lindf  19147  cldval  19814  difopn  19825  mretopd  19884  restcld  19964  ordtcld1  19989  ordtcld2  19990  cnclima  20060  iscncl  20061  isreg2  20169  llycmpkgen2  20341  1stckgen  20345  ptval  20361  txcld  20394  ptcld  20404  txkgen  20443  qtopcld  20504  qtoprest  20508  qtopcmap  20510  kqcldsat  20524  regr1lem  20530  trufil  20701  ufildr  20722  opnsubg  20896  cldsubg  20899  blcld  21298  lebnumlem1  21751  bcthlem1  22053  bcth  22058  bcth3  22060  difmbl  22243  itg1val  22380  itgioo  22512  limciun  22588  dvfval  22591  istrkgl  24232  ishpg  24511  eengv  24686  elntg  24691  isuhgra  24702  isushgra  24705  uhgrac  24709  uhgraeq12d  24711  isumgra  24719  isuslgra  24747  isusgra  24748  usgraeq12d  24766  nb3graprlem2  24856  cusgra3v  24868  isconngra1  25077  frgra3v  25406  difuncomp  27834  imadifxp  27880  gtiso  27949  difico  28028  submarchi  28168  qtophaus  28278  imambfm  28696  difelcarsg  28744  carsgclctunlem1  28751  carsggect  28752  issibf  28767  sibf0  28768  sitgfval  28775  ballotlemfval  28920  ballotlemfp1  28922  ballotlemgun  28955  kur14  29500  iscvm  29543  cvmscld  29557  mdvval  29703  topbnd  30539  mblfinlem3  31405  mblfinlem4  31406  itg2addnclem  31419  itg2addnclem2  31420  aomclem8  35349  kelac2  35353  fzdifsuc2  36861  iccdifioo  36904  iccdifprioo  36905  ibliooicc  37119  dirkercncflem2  37235  isuhgr  37976  isushgr  37977  uhgeq12g  37980  uhguhgra  37982  uhgrauhg  37983  uhg0v  37987  uhgun  37990
  Copyright terms: Public domain W3C validator