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

Theorem difeq1d 3488
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 3482 . 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 1369    \ cdif 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2739  df-dif 3346
This theorem is referenced by:  difeq12d  3490  diftpsn3  4027  dffv2  5779  phplem4  7508  unfilem3  7593  marypha1lem  7698  infdifsn  7877  cantnfp1lem3  7903  cantnfp1lem3OLD  7929  en2other2  8191  isacn  8229  cda1dif  8360  fin23lem28  8524  enfin1ai  8568  fin1a2lem7  8590  fzdifsuc  11531  axdc4uz  11820  leiso  12227  isstruct2  14198  strle1  14284  pltfval  15144  f1omvdco2  15969  symgsssg  15988  symgfisg  15989  symggen  15991  pmtrdifellem3  15999  pmtrdifwrdellem3  16004  pmtrdifwrdel2lem1  16005  pmtrdifwrdel  16006  pmtrdifwrdel2  16007  psgnunilem1  16014  psgnunilem5  16015  psgnunilem2  16016  psgnunilem3  16017  gsumval3OLD  16397  gsumval3  16400  dmdprd  16495  dprd2da  16556  dmdprdsplit2lem  16559  dpjfval  16569  ablfac1eulem  16588  lssset  17030  lbspropd  17195  opsrtoslem2  17581  islindf  18256  islindf2  18258  f1lindf  18266  cldval  18642  difopn  18653  mretopd  18711  restcld  18791  ordtcld1  18816  ordtcld2  18817  cnclima  18887  iscncl  18888  isreg2  18996  llycmpkgen2  19138  1stckgen  19142  ptval  19158  txcld  19191  ptcld  19201  txkgen  19240  qtopcld  19301  qtoprest  19305  qtopcmap  19307  kqcldsat  19321  regr1lem  19327  trufil  19498  ufildr  19519  opnsubg  19693  cldsubg  19696  blcld  20095  lebnumlem1  20548  bcthlem1  20850  bcth  20855  bcth3  20857  difmbl  21039  itg1val  21176  itgioo  21308  limciun  21384  dvfval  21387  istrkgl  22936  eengv  23240  elntg  23245  isuhgra  23252  uhgraeq12d  23256  isumgra  23264  isuslgra  23286  isusgra  23287  usgraeq12d  23299  nb3graprlem2  23375  cusgra3v  23387  isconngra1  23574  imadifxp  25954  gtiso  26011  difico  26088  submarchi  26218  imambfm  26692  issibf  26734  sibf0  26735  sitgfval  26742  ballotlemfval  26887  ballotlemfp1  26889  ballotlemgun  26922  kur14  27119  iscvm  27163  cvmscld  27177  mblfinlem3  28449  mblfinlem4  28450  itg2addnclem  28462  itg2addnclem2  28463  topbnd  28538  aomclem8  29433  kelac2  29437  frgra3v  30613
  Copyright terms: Public domain W3C validator