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

Theorem difeq1d 3306
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 3300 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2syl 15 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    \ cdif 3162
This theorem is referenced by:  difeq12d  3308  diftpsn3  3772  dffv2  5608  phplem4  7059  unfilem3  7139  marypha1lem  7202  infdifsn  7373  cantnfp1lem3  7398  isacn  7687  cda1dif  7818  fin23lem28  7982  enfin1ai  8026  fin1a2lem7  8048  axdc4uz  11061  leiso  11413  isstruct2  13173  strle1  13255  pltfval  14109  gsumval3  15207  dmdprd  15252  dprd2da  15293  dmdprdsplit2lem  15296  dpjfval  15306  ablfac1eulem  15323  lssset  15707  lbspropd  15868  opsrtoslem2  16242  cldval  16776  difopn  16787  mretopd  16845  restcld  16919  ordtcld1  16943  ordtcld2  16944  cnclima  17013  iscncl  17014  isreg2  17121  llycmpkgen2  17261  1stckgen  17265  ptval  17281  txcld  17314  ptcld  17323  txkgen  17362  qtopcld  17420  qtoprest  17424  qtopcmap  17426  kqcldsat  17440  regr1lem  17446  trufil  17621  ufildr  17642  opnsubg  17806  cldsubg  17809  blcld  18067  lebnumlem1  18475  bcthlem1  18762  bcth  18767  bcth3  18769  difmbl  18916  itg1val  19054  itgioo  19186  limciun  19260  dvfval  19263  ballotlemfval  23064  ballotlemfp1  23066  ballotlemgun  23099  gtiso  23256  imambfm  23582  kur14  23762  iscvm  23805  cvmscld  23819  isumgra  23882  itg2addnclem  25003  itg2addnclem2  25004  isder  25810  nds  26253  isside0  26267  aishp  26275  topbnd  26345  aomclem8  27262  kelac2  27266  islindf  27385  islindf2  27387  f1lindf  27395  en2other2  27485  f1omvdco2  27494  symgsssg  27511  symgfisg  27512  symggen  27514  psgnunilem1  27519  psgnunilem5  27520  psgnunilem2  27521  psgnunilem3  27522  isuslgra  28234  isusgra  28235  usgraeq12d  28245  nb3graprlem2  28288  cusgra2v  28297  cusgra3v  28299  frgra2v  28423  frgra3v  28426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-dif 3168
  Copyright terms: Public domain W3C validator