Theorem difeq2d 4075

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 4069	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-dif 3901

This theorem is referenced by:  difeq12d  4076  iinvdif  5032  otiunsndisj  5465  xpdifid  6123  imain  6574  dffv2  6926  f12dfv  7216  f13dfv  7217  tz7.49  8373  oev2  8447  difsnen  8983  domunsncan  9001  sbthlem2  9012  sbthlem3  9013  sbth  9021  rexdif1en  9081  dif1en  9082  sbthfi  9119  phplem2  9125  unblem2  9188  unblem3  9189  dfac8alem  9931  dfac8a  9932  kmlem9  10061  kmlem11  10063  kmlem12  10064  compsscnvlem  10272  s3iunsndisj  14882  isercolllem3  15581  ruclem13  16158  bitsf1  16364  setsvalg  17084  setsval  17085  setsdm  17088  ismri2dad  17551  mreexmrid  17557  mreexexlemd  17558  gsumvalx  18592  gsumpropd  18594  gsumpropd2lem  18595  gsumress  18598  pmtrfv  19372  gsumval3a  19823  gsumval3  19827  dprdcntz  19930  dprddisj  19931  dprdsn  19958  dprddisj2  19961  dpjval  19978  ablfac1eu  19995  drngprop  20668  subdrgint  20727  lbsind  21023  islbs2  21100  lbsextlem4  21107  lbsextg  21108  frlmlbs  21743  lindfind  21762  lindsind  21763  lindfrn  21767  f1lindf  21768  submaval  22516  mdetunilem3  22549  mdetunilem4  22550  mdetunilem9  22555  clsval2  22985  ntrval2  22986  ntrdif  22987  clsdif  22988  cmclsopn  22997  islp  23075  pnrmopn  23278  hauscmplem  23341  bwth  23345  conndisj  23351  cvsunit  25078  bcthlem1  25271  bcth  25276  bcth3  25278  cmmbl  25482  nulmbl2  25484  shftmbl  25486  volsup  25504  mbfimaicc  25579  eldv  25846  ig1pval  26128  tglngval  28549  axlowdimlem15  28955  axlowdim  28960  nbgr2vtx1edg  29349  nbuhgr2vtx1edgb  29351  nb3grprlem2  29380  uvtxel  29387  uvtxel1  29395  uvtxusgrel  29402  cusgredg  29423  cplgr1v  29429  cplgr3v  29434  usgredgsscusgredg  29459  usgr2pthlem  29762  2wspiundisj  29965  frcond1  30267  frgr1v  30272  nfrgr2v  30273  frgr3v  30276  1vwmgr  30277  3vfriswmgr  30279  3cyclfrgrrn1  30286  n4cyclfrgr  30292  frgrwopreglem4a  30311  supppreima  32696  odpmco  33096  tocycfv  33119  tocycf  33127  tocyc01  33128  cycpm2tr  33129  cycpmconjslem2  33165  cyc3conja  33167  0nellinds  33379  lindssn  33387  extvfval  33625  lbslsat  33701  lindsunlem  33709  ist0cld  33918  sigapildsyslem  34246  carsgclctunlem3  34405  sitgval  34417  ballotlemfval  34575  cplgredgex  35237  cvmscbv  35374  cvmsdisj  35386  cvmsss2  35390  satfv1  35479  satffunlem  35517  satffunlem1lem1  35518  satffunlem2lem1  35520  clsun  36444  lindsadd  37726  lindsenlbs  37728  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  cnambfre  37781  watvalN  40165  dnnumch1  43201  aomclem3  43213  aomclem8  43218  safesnsupfilb  43575  dssmapfv2d  44175  dssmapfv3d  44176  dssmapnvod  44177  clsk3nimkb  44197  ntrclscls00  44223  ntrclsiso  44224  ntrclsk3  44227  ntrclsk4  44229  nzprmdif  44476  compne  44597  dvmptfprodlem  46104  fouriercn  46392  meaiininclem  46646  meaiininc  46647  carageniuncllem1  46681  lindslinindsimp2  48625  ldepsnlinc  48670  line  48894  rrxline  48896  iscnrm3rlem4  49104