Theorem difeq2d 4058

Description: Deduction adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
difeq2d	⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Proof of Theorem difeq2d

Step	Hyp	Ref	Expression
1		difeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		difeq2 4052	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-dif 3891

This theorem is referenced by:  difeq12d  4059  iinvdif  5010  otiunsndisj  5435  xpdifid  6076  imain  6526  dffv2  6872  f12dfv  7154  f13dfv  7155  tz7.49  8285  oev2  8362  difsnen  8849  domunsncan  8868  sbthlem2  8880  sbthlem3  8881  sbth  8889  rexdif1en  8953  dif1en  8954  sbthfi  8994  phplem2  9000  phplem3OLD  9011  phplem4OLD  9012  unblem2  9076  unblem3  9077  xpfi  9094  dfac8alem  9794  dfac8a  9795  kmlem9  9923  kmlem11  9925  kmlem12  9926  compsscnvlem  10135  s3iunsndisj  14688  isercolllem3  15387  ruclem13  15960  bitsf1  16162  setsvalg  16876  setsval  16877  setsdm  16880  ismri2dad  17355  mreexmrid  17361  mreexexlemd  17362  gsumvalx  18369  gsumpropd  18371  gsumpropd2lem  18372  gsumress  18375  pmtrfv  19069  gsumval3a  19513  gsumval3  19517  dprdcntz  19620  dprddisj  19621  dprdsn  19648  dprddisj2  19651  dpjval  19668  ablfac1eu  19685  drngprop  20011  subdrgint  20080  lbsind  20351  islbs2  20425  lbsextlem4  20432  lbsextg  20433  frlmlbs  21013  lindfind  21032  lindsind  21033  lindfrn  21037  f1lindf  21038  submaval  21739  mdetunilem3  21772  mdetunilem4  21773  mdetunilem9  21778  clsval2  22210  ntrval2  22211  ntrdif  22212  clsdif  22213  cmclsopn  22222  islp  22300  pnrmopn  22503  hauscmplem  22566  bwth  22570  conndisj  22576  cvsunit  24303  bcthlem1  24497  bcth  24502  bcth3  24504  cmmbl  24707  nulmbl2  24709  shftmbl  24711  volsup  24729  mbfimaicc  24804  eldv  25071  ig1pval  25346  tglngval  26921  axlowdimlem15  27333  axlowdim  27338  nbgr2vtx1edg  27726  nbuhgr2vtx1edgb  27728  nb3grprlem2  27757  uvtxel  27764  uvtxel1  27772  uvtxusgrel  27779  cusgredg  27800  cplgr1v  27806  cplgr3v  27811  usgredgsscusgredg  27835  usgr2pthlem  28140  2wspiundisj  28337  frcond1  28639  frgr1v  28644  nfrgr2v  28645  frgr3v  28648  1vwmgr  28649  3vfriswmgr  28651  3cyclfrgrrn1  28658  n4cyclfrgr  28664  frgrwopreglem4a  28683  supppreima  31034  odpmco  31364  tocycfv  31385  tocycf  31393  tocyc01  31394  cycpm2tr  31395  cycpmconjslem2  31431  cyc3conja  31433  0nellinds  31575  lindssn  31582  lbslsat  31708  lindsunlem  31714  ist0cld  31792  sigapildsyslem  32138  carsgclctunlem3  32296  sitgval  32308  ballotlemfval  32465  cplgredgex  33091  cvmscbv  33229  cvmsdisj  33241  cvmsss2  33245  satfv1  33334  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  clsun  34526  lindsadd  35779  lindsenlbs  35781  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  cnambfre  35834  watvalN  38014  dnnumch1  40876  aomclem3  40888  aomclem8  40893  dssmapfv2d  41633  dssmapfv3d  41634  dssmapnvod  41635  clsk3nimkb  41657  ntrclscls00  41683  ntrclsiso  41684  ntrclsk3  41687  ntrclsk4  41689  nzprmdif  41944  compne  42066  dvmptfprodlem  43492  fouriercn  43780  meaiininclem  44031  meaiininc  44032  carageniuncllem1  44066  lindslinindsimp2  45815  ldepsnlinc  45860  line  46089  rrxline  46091  iscnrm3rlem4  46248