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

Theorem difeq1d 3606
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 3600 . 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 1383    \ cdif 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-dif 3464
This theorem is referenced by:  difeq12d  3608  diftpsn3  4153  dffv2  5931  phplem4  7701  unfilem3  7788  marypha1lem  7895  infdifsn  8076  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  en2other2  8390  isacn  8428  cda1dif  8559  fin23lem28  8723  enfin1ai  8767  fin1a2lem7  8789  fzdifsuc  11750  axdc4uz  12075  leiso  12490  isstruct2  14623  strle1  14710  pltfval  15568  f1omvdco2  16452  symgsssg  16471  symgfisg  16472  symggen  16474  pmtrdifellem3  16482  pmtrdifwrdellem3  16487  pmtrdifwrdel2lem1  16488  pmtrdifwrdel  16489  pmtrdifwrdel2  16490  psgnunilem1  16497  psgnunilem5  16498  psgnunilem2  16499  psgnunilem3  16500  gsumval3OLD  16887  gsumval3  16890  dmdprd  17008  dprd2da  17070  dmdprdsplit2lem  17073  dpjfval  17083  ablfac1eulem  17102  lssset  17559  lbspropd  17724  opsrtoslem2  18128  islindf  18825  islindf2  18827  f1lindf  18835  cldval  19502  difopn  19513  mretopd  19571  restcld  19651  ordtcld1  19676  ordtcld2  19677  cnclima  19747  iscncl  19748  isreg2  19856  llycmpkgen2  20029  1stckgen  20033  ptval  20049  txcld  20082  ptcld  20092  txkgen  20131  qtopcld  20192  qtoprest  20196  qtopcmap  20198  kqcldsat  20212  regr1lem  20218  trufil  20389  ufildr  20410  opnsubg  20584  cldsubg  20587  blcld  20986  lebnumlem1  21439  bcthlem1  21741  bcth  21746  bcth3  21748  difmbl  21931  itg1val  22068  itgioo  22200  limciun  22276  dvfval  22279  istrkgl  23833  ishpg  24106  eengv  24260  elntg  24265  isuhgra  24276  isushgra  24279  uhgrac  24283  uhgraeq12d  24285  isumgra  24293  isuslgra  24321  isusgra  24322  usgraeq12d  24340  nb3graprlem2  24430  cusgra3v  24442  isconngra1  24651  frgra3v  24980  imadifxp  27436  gtiso  27497  difico  27572  submarchi  27708  qtophaus  27817  imambfm  28211  issibf  28253  sibf0  28254  sitgfval  28261  ballotlemfval  28406  ballotlemfp1  28408  ballotlemgun  28441  kur14  28638  iscvm  28682  cvmscld  28696  mdvval  28842  mblfinlem3  30029  mblfinlem4  30030  itg2addnclem  30042  itg2addnclem2  30043  topbnd  30118  aomclem8  30983  kelac2  30987  fzdifsuc2  31466  iccdifioo  31509  iccdifprioo  31510  ibliooicc  31724  dirkercncflem2  31840  isuhgr  32320  isushgr  32321  uhgeq12g  32324  uhguhgra  32326  uhgrauhg  32327  uhg0v  32331  uhgun  32334
  Copyright terms: Public domain W3C validator