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

Theorem difeq1d 3582
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 3576 . 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 1437    \ cdif 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-dif 3439
This theorem is referenced by:  difeq12d  3584  diftpsn3  4138  dffv2  5954  phplem4  7763  unfilem3  7846  marypha1lem  7956  infdifsn  8170  cantnfp1lem3  8193  en2other2  8448  isacn  8482  cda1dif  8613  fin23lem28  8777  enfin1ai  8821  fin1a2lem7  8843  fzdifsuc  11862  axdc4uz  12202  leiso  12626  isstruct2  15129  strle1  15220  pltfval  16204  f1omvdco2  17088  symgsssg  17107  symgfisg  17108  symggen  17110  pmtrdifellem3  17118  pmtrdifwrdellem3  17123  pmtrdifwrdel2lem1  17124  pmtrdifwrdel  17125  pmtrdifwrdel2  17126  psgnunilem1  17133  psgnunilem5  17134  psgnunilem2  17135  psgnunilem3  17136  gsumval3  17540  dmdprd  17629  dprd2da  17674  dmdprdsplit2lem  17677  dpjfval  17687  ablfac1eulem  17704  lssset  18156  lbspropd  18321  opsrtoslem2  18707  islindf  19368  islindf2  19370  f1lindf  19378  cldval  20036  difopn  20047  mretopd  20106  restcld  20186  ordtcld1  20211  ordtcld2  20212  cnclima  20282  iscncl  20283  isreg2  20391  llycmpkgen2  20563  1stckgen  20567  ptval  20583  txcld  20616  ptcld  20626  txkgen  20665  qtopcld  20726  qtoprest  20730  qtopcmap  20732  kqcldsat  20746  regr1lem  20752  trufil  20923  ufildr  20944  opnsubg  21120  cldsubg  21123  blcld  21518  lebnumlem1  21987  lebnumlem1OLD  21990  bcthlem1  22290  bcth  22295  bcth3  22297  difmbl  22494  itg1val  22639  itgioo  22771  limciun  22847  dvfval  22850  istrkgl  24504  ishpg  24799  eengv  25007  elntg  25012  isuhgra  25023  isushgra  25026  uhgrac  25030  uhgraeq12d  25032  isumgra  25040  isuslgra  25068  isusgra  25069  usgraeq12d  25087  nb3graprlem2  25178  cusgra3v  25190  isconngra1  25399  frgra3v  25728  difuncomp  28168  imadifxp  28214  gtiso  28283  difico  28371  fzdif2  28375  submarchi  28510  qtophaus  28671  imambfm  29092  difelcarsg  29150  carsgclctunlem1  29157  carsggect  29158  issibf  29174  sibf0  29175  sitgfval  29182  ballotlemfval  29330  ballotlemfp1  29332  ballotlemgun  29365  ballotlemgunOLD  29403  kur14  29947  iscvm  29990  cvmscld  30004  mdvval  30150  topbnd  30985  poimirlem2  31906  poimirlem4  31908  poimirlem6  31910  poimirlem7  31911  poimirlem8  31912  poimirlem11  31915  poimirlem12  31916  poimirlem13  31917  poimirlem14  31918  poimirlem16  31920  poimirlem18  31922  poimirlem19  31923  poimirlem21  31925  poimirlem22  31926  poimirlem23  31927  poimirlem27  31931  poimirlem30  31934  mblfinlem3  31943  mblfinlem4  31944  itg2addnclem  31957  itg2addnclem2  31958  aomclem8  35889  kelac2  35893  fzdifsuc2  37484  iccdifioo  37565  iccdifprioo  37566  ibliooicc  37788  dirkercncflem2  37906  issal  38096  prsal  38100  saldifcl2  38108  intsal  38110  sge0fodjrnlem  38166  caratheodorylem1  38255  isuhgr  38980  isushgr  38981  uhgreq12g  38987  uhgruhgra  38989  uhgrauhgr  38990  uhgrop  38992  uhgr0v  38994  uhgrun  38997  isumgr  39003  umgrun  39020  isuspgr  39032  isusgr  39033  usgr1vr  39105  nb3grprlem2  39214  uvtxaval  39218  nbumgruvtxres  39236  cplgrop  39260  cusgrexi  39263  isuhgrALTV  39297  isushgrALTV  39298  uhgeq12gALTV  39301  uhguhgra  39303  uhgrauhg  39304  uhg0v  39308  uhgun  39311
  Copyright terms: Public domain W3C validator