Theorem difeq2d 4089

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-dif 3917

This theorem is referenced by:  difeq12d  4090  iinvdif  5044  otiunsndisj  5480  xpdifid  6141  imain  6601  dffv2  6956  f12dfv  7248  f13dfv  7249  tz7.49  8413  oev2  8487  difsnen  9023  domunsncan  9041  sbthlem2  9052  sbthlem3  9053  sbth  9061  rexdif1en  9122  rexdif1enOLD  9123  dif1en  9124  dif1enOLD  9126  sbthfi  9163  phplem2  9169  unblem2  9240  unblem3  9241  xpfiOLD  9270  dfac8alem  9982  dfac8a  9983  kmlem9  10112  kmlem11  10114  kmlem12  10115  compsscnvlem  10323  s3iunsndisj  14934  isercolllem3  15633  ruclem13  16210  bitsf1  16416  setsvalg  17136  setsval  17137  setsdm  17140  ismri2dad  17598  mreexmrid  17604  mreexexlemd  17605  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  pmtrfv  19382  gsumval3a  19833  gsumval3  19837  dprdcntz  19940  dprddisj  19941  dprdsn  19968  dprddisj2  19971  dpjval  19988  ablfac1eu  20005  drngprop  20653  subdrgint  20712  lbsind  20987  islbs2  21064  lbsextlem4  21071  lbsextg  21072  frlmlbs  21706  lindfind  21725  lindsind  21726  lindfrn  21730  f1lindf  21731  submaval  22468  mdetunilem3  22501  mdetunilem4  22502  mdetunilem9  22507  clsval2  22937  ntrval2  22938  ntrdif  22939  clsdif  22940  cmclsopn  22949  islp  23027  pnrmopn  23230  hauscmplem  23293  bwth  23297  conndisj  23303  cvsunit  25031  bcthlem1  25224  bcth  25229  bcth3  25231  cmmbl  25435  nulmbl2  25437  shftmbl  25439  volsup  25457  mbfimaicc  25532  eldv  25799  ig1pval  26081  tglngval  28478  axlowdimlem15  28883  axlowdim  28888  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  nb3grprlem2  29308  uvtxel  29315  uvtxel1  29323  uvtxusgrel  29330  cusgredg  29351  cplgr1v  29357  cplgr3v  29362  usgredgsscusgredg  29387  usgr2pthlem  29693  2wspiundisj  29893  frcond1  30195  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  1vwmgr  30205  3vfriswmgr  30207  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrwopreglem4a  30239  supppreima  32614  odpmco  33043  tocycfv  33066  tocycf  33074  tocyc01  33075  cycpm2tr  33076  cycpmconjslem2  33112  cyc3conja  33114  0nellinds  33341  lindssn  33349  lbslsat  33612  lindsunlem  33620  ist0cld  33823  sigapildsyslem  34151  carsgclctunlem3  34311  sitgval  34323  ballotlemfval  34481  cplgredgex  35108  cvmscbv  35245  cvmsdisj  35257  cvmsss2  35261  satfv1  35350  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  clsun  36316  lindsadd  37607  lindsenlbs  37609  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  cnambfre  37662  watvalN  39987  dnnumch1  43033  aomclem3  43045  aomclem8  43050  safesnsupfilb  43407  dssmapfv2d  44007  dssmapfv3d  44008  dssmapnvod  44009  clsk3nimkb  44029  ntrclscls00  44055  ntrclsiso  44056  ntrclsk3  44059  ntrclsk4  44061  nzprmdif  44308  compne  44430  dvmptfprodlem  45942  fouriercn  46230  meaiininclem  46484  meaiininc  46485  carageniuncllem1  46519  lindslinindsimp2  48452  ldepsnlinc  48497  line  48721  rrxline  48723  iscnrm3rlem4  48931