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

Theorem difeq1d 3293
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 3287 . 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 1623    \ cdif 3149
This theorem is referenced by:  difeq12d  3295  dffv2  5592  phplem4  7043  unfilem3  7123  marypha1lem  7186  infdifsn  7357  cantnfp1lem3  7382  isacn  7671  cda1dif  7802  fin23lem28  7966  enfin1ai  8010  fin1a2lem7  8032  axdc4uz  11045  leiso  11397  isstruct2  13157  strle1  13239  pltfval  14093  gsumval3  15191  dmdprd  15236  dprd2da  15277  dmdprdsplit2lem  15280  dpjfval  15290  ablfac1eulem  15307  lssset  15691  lbspropd  15852  opsrtoslem2  16226  cldval  16760  difopn  16771  mretopd  16829  restcld  16903  ordtcld1  16927  ordtcld2  16928  cnclima  16997  iscncl  16998  isreg2  17105  llycmpkgen2  17245  1stckgen  17249  ptval  17265  txcld  17298  ptcld  17307  txkgen  17346  qtopcld  17404  qtoprest  17408  qtopcmap  17410  kqcldsat  17424  regr1lem  17430  trufil  17605  ufildr  17626  opnsubg  17790  cldsubg  17793  blcld  18051  lebnumlem1  18459  bcthlem1  18746  bcth  18751  bcth3  18753  difmbl  18900  itg1val  19038  itgioo  19170  limciun  19244  dvfval  19247  ballotlemfval  23048  ballotlemfp1  23050  ballotlemgun  23083  gtiso  23241  imambfm  23567  kur14  23747  iscvm  23790  cvmscld  23804  isumgra  23867  isder  25707  nds  26150  isside0  26164  aishp  26172  topbnd  26242  aomclem8  27159  kelac2  27163  islindf  27282  islindf2  27284  f1lindf  27292  en2other2  27382  f1omvdco2  27391  symgsssg  27408  symgfisg  27409  symggen  27411  psgnunilem1  27416  psgnunilem5  27417  psgnunilem2  27418  psgnunilem3  27419  difprsneq  28068  diftpsneq  28070  isuslgra  28102  isusgra  28103  usgraeq12d  28111  cusgra2v  28158  frgra2v  28177  frgra3v  28180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-dif 3155
  Copyright terms: Public domain W3C validator