Theorem difeq2d 4067

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-dif 3893

This theorem is referenced by:  difeq12d  4068  iinvdif  5023  otiunsndisj  5468  xpdifid  6126  imain  6577  dffv2  6929  f12dfv  7221  f13dfv  7222  tz7.49  8377  oev2  8451  difsnen  8990  domunsncan  9008  sbthlem2  9019  sbthlem3  9020  sbth  9028  rexdif1en  9088  dif1en  9089  sbthfi  9126  phplem2  9132  unblem2  9196  unblem3  9197  dfac8alem  9942  dfac8a  9943  kmlem9  10072  kmlem11  10074  kmlem12  10075  compsscnvlem  10283  s3iunsndisj  14921  isercolllem3  15620  ruclem13  16200  bitsf1  16406  setsvalg  17127  setsval  17128  setsdm  17131  ismri2dad  17594  mreexmrid  17600  mreexexlemd  17601  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  pmtrfv  19418  gsumval3a  19869  gsumval3  19873  dprdcntz  19976  dprddisj  19977  dprdsn  20004  dprddisj2  20007  dpjval  20024  ablfac1eu  20041  drngprop  20712  subdrgint  20771  lbsind  21067  islbs2  21144  lbsextlem4  21151  lbsextg  21152  frlmlbs  21787  lindfind  21806  lindsind  21807  lindfrn  21811  f1lindf  21812  submaval  22556  mdetunilem3  22589  mdetunilem4  22590  mdetunilem9  22595  clsval2  23025  ntrval2  23026  ntrdif  23027  clsdif  23028  cmclsopn  23037  islp  23115  pnrmopn  23318  hauscmplem  23381  bwth  23385  conndisj  23391  cvsunit  25108  bcthlem1  25301  bcth  25306  bcth3  25308  cmmbl  25511  nulmbl2  25513  shftmbl  25515  volsup  25533  mbfimaicc  25608  eldv  25875  ig1pval  26151  tglngval  28633  axlowdimlem15  29039  axlowdim  29044  nbgr2vtx1edg  29433  nbuhgr2vtx1edgb  29435  nb3grprlem2  29464  uvtxel  29471  uvtxel1  29479  uvtxusgrel  29486  cusgredg  29507  cplgr1v  29513  cplgr3v  29518  usgredgsscusgredg  29543  usgr2pthlem  29846  2wspiundisj  30049  frcond1  30351  frgr1v  30356  nfrgr2v  30357  frgr3v  30360  1vwmgr  30361  3vfriswmgr  30363  3cyclfrgrrn1  30370  n4cyclfrgr  30376  frgrwopreglem4a  30395  supppreima  32779  odpmco  33162  tocycfv  33185  tocycf  33193  tocyc01  33194  cycpm2tr  33195  cycpmconjslem2  33231  cyc3conja  33233  0nellinds  33445  lindssn  33453  extvfval  33691  lbslsat  33776  lindsunlem  33784  ist0cld  33993  sigapildsyslem  34321  carsgclctunlem3  34480  sitgval  34492  ballotlemfval  34650  cplgredgex  35319  cvmscbv  35456  cvmsdisj  35468  cvmsss2  35472  satfv1  35561  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  clsun  36526  lindsadd  37948  lindsenlbs  37950  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  cnambfre  38003  watvalN  40453  dnnumch1  43490  aomclem3  43502  aomclem8  43507  safesnsupfilb  43863  dssmapfv2d  44463  dssmapfv3d  44464  dssmapnvod  44465  clsk3nimkb  44485  ntrclscls00  44511  ntrclsiso  44512  ntrclsk3  44515  ntrclsk4  44517  nzprmdif  44764  compne  44885  dvmptfprodlem  46390  fouriercn  46678  meaiininclem  46932  meaiininc  46933  carageniuncllem1  46967  lindslinindsimp2  48951  ldepsnlinc  48996  line  49220  rrxline  49222  iscnrm3rlem4  49430