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

Theorem difeq1d 3562
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 3556 . 2  |-  ( A  =  B  ->  ( A  \  C )  =  ( B  \  C
) )
31, 2syl 17 1  |-  ( ph  ->  ( A  \  C
)  =  ( B 
\  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    \ cdif 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-dif 3419
This theorem is referenced by:  difeq12d  3564  diftpsn3  4123  dffv2  5966  phplem4  7785  unfilem3  7868  marypha1lem  7978  infdifsn  8193  cantnfp1lem3  8216  en2other2  8471  isacn  8506  cda1dif  8637  fin23lem28  8801  enfin1ai  8845  fin1a2lem7  8867  fzdifsuc  11890  axdc4uz  12234  leiso  12661  isstruct2  15185  strle1  15276  pltfval  16260  f1omvdco2  17144  symgsssg  17163  symgfisg  17164  symggen  17166  pmtrdifellem3  17174  pmtrdifwrdellem3  17179  pmtrdifwrdel2lem1  17180  pmtrdifwrdel  17181  pmtrdifwrdel2  17182  psgnunilem1  17189  psgnunilem5  17190  psgnunilem2  17191  psgnunilem3  17192  gsumval3  17596  dmdprd  17685  dprd2da  17730  dmdprdsplit2lem  17733  dpjfval  17743  ablfac1eulem  17760  lssset  18212  lbspropd  18377  opsrtoslem2  18763  islindf  19425  islindf2  19427  f1lindf  19435  cldval  20093  difopn  20104  mretopd  20163  restcld  20243  ordtcld1  20268  ordtcld2  20269  cnclima  20339  iscncl  20340  isreg2  20448  llycmpkgen2  20620  1stckgen  20624  ptval  20640  txcld  20673  ptcld  20683  txkgen  20722  qtopcld  20783  qtoprest  20787  qtopcmap  20789  kqcldsat  20803  regr1lem  20809  trufil  20980  ufildr  21001  opnsubg  21177  cldsubg  21180  blcld  21575  lebnumlem1  22044  lebnumlem1OLD  22047  bcthlem1  22347  bcth  22352  bcth3  22354  difmbl  22552  itg1val  22697  itgioo  22829  limciun  22905  dvfval  22908  istrkgl  24562  ishpg  24857  eengv  25065  elntg  25070  isuhgra  25081  isushgra  25084  uhgrac  25088  uhgraeq12d  25090  isumgra  25098  isuslgra  25126  isusgra  25127  usgraeq12d  25145  nb3graprlem2  25236  cusgra3v  25248  isconngra1  25457  frgra3v  25786  difuncomp  28221  imadifxp  28265  gtiso  28333  difico  28417  fzdif2  28421  submarchi  28554  qtophaus  28714  imambfm  29134  difelcarsg  29192  carsgclctunlem1  29199  carsggect  29200  issibf  29216  sibf0  29217  sitgfval  29224  ballotlemfval  29372  ballotlemfp1  29374  ballotlemgun  29407  ballotlemgunOLD  29445  kur14  29989  iscvm  30032  cvmscld  30046  mdvval  30192  topbnd  31030  poimirlem2  31988  poimirlem4  31990  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem11  31997  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem16  32002  poimirlem18  32004  poimirlem19  32005  poimirlem21  32007  poimirlem22  32008  poimirlem23  32009  poimirlem27  32013  poimirlem30  32016  mblfinlem3  32025  mblfinlem4  32026  itg2addnclem  32039  itg2addnclem2  32040  aomclem8  35965  kelac2  35969  fzdifsuc2  37605  iccdifioo  37701  iccdifprioo  37702  ibliooicc  37934  dirkercncflem2  38067  issal  38276  prsal  38280  saldifcl2  38288  intsal  38290  sge0fodjrnlem  38361  caratheodorylem1  38455  vonvolmbllem  38589  isuhgr  39293  isushgr  39294  uhgreq12g  39298  uhgruhgra  39303  uhgrauhgr  39304  isuhgrop  39306  uhgr0vb  39308  uhgrun  39310  isupgr  39319  isumgr  39328  upgrun  39350  isuspgr  39383  isusgr  39384  usgr1vr  39475  nb3grprlem2  39601  uvtxaval  39605  nbupgruvtxres  39626  cplgrop  39650  cusgrexi  39653  uspgrloopnb0  39702  isconngr1  40027  isuhgrALTV  40047  isushgrALTV  40048  uhgeq12gALTV  40051  uhguhgra  40053  uhgrauhg  40054  uhg0v  40058  uhgun  40061
  Copyright terms: Public domain W3C validator