Theorem difeq2d 4122

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

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

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-dif 3951

This theorem is referenced by:  difeq12d  4123  iinvdif  5083  otiunsndisj  5520  xpdifid  6167  imain  6633  dffv2  6986  f12dfv  7274  f13dfv  7275  tz7.49  8451  oev2  8529  difsnen  9059  domunsncan  9078  sbthlem2  9090  sbthlem3  9091  sbth  9099  rexdif1en  9164  rexdif1enOLD  9165  dif1en  9166  dif1enOLD  9168  sbthfi  9208  phplem2  9214  phplem3OLD  9225  phplem4OLD  9226  unblem2  9302  unblem3  9303  xpfiOLD  9324  dfac8alem  10030  dfac8a  10031  kmlem9  10159  kmlem11  10161  kmlem12  10162  compsscnvlem  10371  s3iunsndisj  14922  isercolllem3  15620  ruclem13  16192  bitsf1  16394  setsvalg  17106  setsval  17107  setsdm  17110  ismri2dad  17588  mreexmrid  17594  mreexexlemd  17595  gsumvalx  18607  gsumpropd  18609  gsumpropd2lem  18610  gsumress  18613  pmtrfv  19368  gsumval3a  19819  gsumval3  19823  dprdcntz  19926  dprddisj  19927  dprdsn  19954  dprddisj2  19957  dpjval  19974  ablfac1eu  19991  drngprop  20598  subdrgint  20650  lbsind  20924  islbs2  21001  lbsextlem4  21008  lbsextg  21009  frlmlbs  21662  lindfind  21681  lindsind  21682  lindfrn  21686  f1lindf  21687  submaval  22403  mdetunilem3  22436  mdetunilem4  22437  mdetunilem9  22442  clsval2  22874  ntrval2  22875  ntrdif  22876  clsdif  22877  cmclsopn  22886  islp  22964  pnrmopn  23167  hauscmplem  23230  bwth  23234  conndisj  23240  cvsunit  24978  bcthlem1  25172  bcth  25177  bcth3  25179  cmmbl  25383  nulmbl2  25385  shftmbl  25387  volsup  25405  mbfimaicc  25480  eldv  25747  ig1pval  26028  tglngval  28235  axlowdimlem15  28647  axlowdim  28652  nbgr2vtx1edg  29040  nbuhgr2vtx1edgb  29042  nb3grprlem2  29071  uvtxel  29078  uvtxel1  29086  uvtxusgrel  29093  cusgredg  29114  cplgr1v  29120  cplgr3v  29125  usgredgsscusgredg  29149  usgr2pthlem  29453  2wspiundisj  29650  frcond1  29952  frgr1v  29957  nfrgr2v  29958  frgr3v  29961  1vwmgr  29962  3vfriswmgr  29964  3cyclfrgrrn1  29971  n4cyclfrgr  29977  frgrwopreglem4a  29996  supppreima  32346  odpmco  32683  tocycfv  32704  tocycf  32712  tocyc01  32713  cycpm2tr  32714  cycpmconjslem2  32750  cyc3conja  32752  0nellinds  32923  lindssn  32934  lbslsat  33155  lindsunlem  33163  ist0cld  33277  sigapildsyslem  33623  carsgclctunlem3  33783  sitgval  33795  ballotlemfval  33952  cplgredgex  34575  cvmscbv  34713  cvmsdisj  34725  cvmsss2  34729  satfv1  34818  satffunlem  34856  satffunlem1lem1  34857  satffunlem2lem1  34859  clsun  35677  lindsadd  36945  lindsenlbs  36947  poimirlem25  36977  poimirlem26  36978  poimirlem27  36979  cnambfre  37000  watvalN  39328  dnnumch1  42249  aomclem3  42261  aomclem8  42266  safesnsupfilb  42632  dssmapfv2d  43232  dssmapfv3d  43233  dssmapnvod  43234  clsk3nimkb  43254  ntrclscls00  43280  ntrclsiso  43281  ntrclsk3  43284  ntrclsk4  43286  nzprmdif  43541  compne  43663  dvmptfprodlem  45119  fouriercn  45407  meaiininclem  45661  meaiininc  45662  carageniuncllem1  45696  lindslinindsimp2  47306  ldepsnlinc  47351  line  47580  rrxline  47582  iscnrm3rlem4  47738