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

Theorem difeq1d 3466
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 3460 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2syl 16 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    \ cdif 3319
This theorem is referenced by:  difeq12d  3468  diftpsn3  3939  dffv2  5798  phplem4  7291  unfilem3  7375  marypha1lem  7440  infdifsn  7613  cantnfp1lem3  7638  isacn  7927  cda1dif  8058  fin23lem28  8222  enfin1ai  8266  fin1a2lem7  8288  axdc4uz  11324  leiso  11710  isstruct2  13480  strle1  13562  pltfval  14418  gsumval3  15516  dmdprd  15561  dprd2da  15602  dmdprdsplit2lem  15605  dpjfval  15615  ablfac1eulem  15632  lssset  16012  lbspropd  16173  opsrtoslem2  16547  cldval  17089  difopn  17100  mretopd  17158  restcld  17238  ordtcld1  17263  ordtcld2  17264  cnclima  17334  iscncl  17335  isreg2  17443  llycmpkgen2  17584  1stckgen  17588  ptval  17604  txcld  17637  ptcld  17647  txkgen  17686  qtopcld  17747  qtoprest  17751  qtopcmap  17753  kqcldsat  17767  regr1lem  17773  trufil  17944  ufildr  17965  opnsubg  18139  cldsubg  18142  blcld  18537  lebnumlem1  18988  bcthlem1  19279  bcth  19284  bcth3  19286  difmbl  19439  itg1val  19577  itgioo  19709  limciun  19783  dvfval  19786  isuhgra  21340  uhgraeq12d  21344  isumgra  21352  isuslgra  21374  isusgra  21375  usgraeq12d  21387  nb3graprlem2  21463  cusgra3v  21475  isconngra1  21662  imadifxp  24040  gtiso  24090  difico  24148  imambfm  24614  issibf  24650  sibf0  24651  sitgfval  24657  ballotlemfval  24749  ballotlemfp1  24751  ballotlemgun  24784  kur14  24904  iscvm  24948  cvmscld  24962  mblfinlem3  26247  mblfinlem4  26248  itg2addnclem  26258  itg2addnclem2  26259  topbnd  26329  aomclem8  27138  kelac2  27142  islindf  27261  islindf2  27263  f1lindf  27271  en2other2  27361  f1omvdco2  27370  symgsssg  27387  symgfisg  27388  symggen  27390  psgnunilem1  27395  psgnunilem5  27396  psgnunilem2  27397  psgnunilem3  27398  frgra3v  28454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-dif 3325
  Copyright terms: Public domain W3C validator