Theorem difeq2d 4023

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

Syntax hints:   → wi 4   = wceq 1543   ∖ cdif 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-dif 3856

This theorem is referenced by:  difeq12d  4024  iinvdif  4974  otiunsndisj  5388  xpdifid  6011  imain  6443  dffv2  6784  f12dfv  7062  f13dfv  7063  tz7.49  8159  oev2  8228  difsnen  8705  domunsncan  8723  sbthlem2  8735  sbthlem3  8736  sbth  8744  phplem3  8805  phplem4  8806  rexdif1en  8817  dif1en  8818  unblem2  8902  unblem3  8903  xpfi  8920  dfac8alem  9608  dfac8a  9609  kmlem9  9737  kmlem11  9739  kmlem12  9740  compsscnvlem  9949  s3iunsndisj  14496  isercolllem3  15195  ruclem13  15766  bitsf1  15968  setsvalg  16694  setsval  16695  setsdm  16699  ismri2dad  17094  mreexmrid  17100  mreexexlemd  17101  gsumvalx  18102  gsumpropd  18104  gsumpropd2lem  18105  gsumress  18108  pmtrfv  18798  gsumval3a  19242  gsumval3  19246  dprdcntz  19349  dprddisj  19350  dprdsn  19377  dprddisj2  19380  dpjval  19397  ablfac1eu  19414  drngprop  19732  subdrgint  19801  lbsind  20071  islbs2  20145  lbsextlem4  20152  lbsextg  20153  frlmlbs  20713  lindfind  20732  lindsind  20733  lindfrn  20737  f1lindf  20738  submaval  21432  mdetunilem3  21465  mdetunilem4  21466  mdetunilem9  21471  clsval2  21901  ntrval2  21902  ntrdif  21903  clsdif  21904  cmclsopn  21913  islp  21991  pnrmopn  22194  hauscmplem  22257  bwth  22261  conndisj  22267  cvsunit  23982  bcthlem1  24175  bcth  24180  bcth3  24182  cmmbl  24385  nulmbl2  24387  shftmbl  24389  volsup  24407  mbfimaicc  24482  eldv  24749  ig1pval  25024  tglngval  26596  axlowdimlem15  27001  axlowdim  27006  nbgr2vtx1edg  27392  nbuhgr2vtx1edgb  27394  nb3grprlem2  27423  uvtxel  27430  uvtxel1  27438  uvtxusgrel  27445  cusgredg  27466  cplgr1v  27472  cplgr3v  27477  usgredgsscusgredg  27501  usgr2pthlem  27804  2wspiundisj  28001  frcond1  28303  frgr1v  28308  nfrgr2v  28309  frgr3v  28312  1vwmgr  28313  3vfriswmgr  28315  3cyclfrgrrn1  28322  n4cyclfrgr  28328  frgrwopreglem4a  28347  supppreima  30699  odpmco  31028  tocycfv  31049  tocycf  31057  tocyc01  31058  cycpm2tr  31059  cycpmconjslem2  31095  cyc3conja  31097  0nellinds  31234  lindssn  31241  lbslsat  31367  lindsunlem  31373  ist0cld  31451  sigapildsyslem  31795  carsgclctunlem3  31953  sitgval  31965  ballotlemfval  32122  cplgredgex  32749  cvmscbv  32887  cvmsdisj  32899  cvmsss2  32903  satfv1  32992  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  clsun  34203  lindsadd  35456  lindsenlbs  35458  poimirlem25  35488  poimirlem26  35489  poimirlem27  35490  cnambfre  35511  watvalN  37693  dnnumch1  40513  aomclem3  40525  aomclem8  40530  dssmapfv2d  41244  dssmapfv3d  41245  dssmapnvod  41246  clsk3nimkb  41268  ntrclscls00  41294  ntrclsiso  41295  ntrclsk3  41298  ntrclsk4  41300  nzprmdif  41551  compne  41673  dvmptfprodlem  43103  fouriercn  43391  meaiininclem  43642  meaiininc  43643  carageniuncllem1  43677  lindslinindsimp2  45420  ldepsnlinc  45465  line  45694  rrxline  45696  iscnrm3rlem4  45853