Theorem difeq2d 4078

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904

This theorem is referenced by:  difeq12d  4079  iinvdif  5035  otiunsndisj  5468  xpdifid  6126  imain  6577  dffv2  6929  f12dfv  7219  f13dfv  7220  tz7.49  8376  oev2  8450  difsnen  8987  domunsncan  9005  sbthlem2  9016  sbthlem3  9017  sbth  9025  rexdif1en  9085  dif1en  9086  sbthfi  9123  phplem2  9129  unblem2  9193  unblem3  9194  dfac8alem  9939  dfac8a  9940  kmlem9  10069  kmlem11  10071  kmlem12  10072  compsscnvlem  10280  s3iunsndisj  14891  isercolllem3  15590  ruclem13  16167  bitsf1  16373  setsvalg  17093  setsval  17094  setsdm  17097  ismri2dad  17560  mreexmrid  17566  mreexexlemd  17567  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  pmtrfv  19381  gsumval3a  19832  gsumval3  19836  dprdcntz  19939  dprddisj  19940  dprdsn  19967  dprddisj2  19970  dpjval  19987  ablfac1eu  20004  drngprop  20677  subdrgint  20736  lbsind  21032  islbs2  21109  lbsextlem4  21116  lbsextg  21117  frlmlbs  21752  lindfind  21771  lindsind  21772  lindfrn  21776  f1lindf  21777  submaval  22525  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  clsval2  22994  ntrval2  22995  ntrdif  22996  clsdif  22997  cmclsopn  23006  islp  23084  pnrmopn  23287  hauscmplem  23350  bwth  23354  conndisj  23360  cvsunit  25087  bcthlem1  25280  bcth  25285  bcth3  25287  cmmbl  25491  nulmbl2  25493  shftmbl  25495  volsup  25513  mbfimaicc  25588  eldv  25855  ig1pval  26137  tglngval  28623  axlowdimlem15  29029  axlowdim  29034  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  nb3grprlem2  29454  uvtxel  29461  uvtxel1  29469  uvtxusgrel  29476  cusgredg  29497  cplgr1v  29503  cplgr3v  29508  usgredgsscusgredg  29533  usgr2pthlem  29836  2wspiundisj  30039  frcond1  30341  frgr1v  30346  nfrgr2v  30347  frgr3v  30350  1vwmgr  30351  3vfriswmgr  30353  3cyclfrgrrn1  30360  n4cyclfrgr  30366  frgrwopreglem4a  30385  supppreima  32770  odpmco  33168  tocycfv  33191  tocycf  33199  tocyc01  33200  cycpm2tr  33201  cycpmconjslem2  33237  cyc3conja  33239  0nellinds  33451  lindssn  33459  extvfval  33697  lbslsat  33773  lindsunlem  33781  ist0cld  33990  sigapildsyslem  34318  carsgclctunlem3  34477  sitgval  34489  ballotlemfval  34647  cplgredgex  35315  cvmscbv  35452  cvmsdisj  35464  cvmsss2  35468  satfv1  35557  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  clsun  36522  lindsadd  37814  lindsenlbs  37816  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  cnambfre  37869  watvalN  40253  dnnumch1  43286  aomclem3  43298  aomclem8  43303  safesnsupfilb  43659  dssmapfv2d  44259  dssmapfv3d  44260  dssmapnvod  44261  clsk3nimkb  44281  ntrclscls00  44307  ntrclsiso  44308  ntrclsk3  44311  ntrclsk4  44313  nzprmdif  44560  compne  44681  dvmptfprodlem  46188  fouriercn  46476  meaiininclem  46730  meaiininc  46731  carageniuncllem1  46765  lindslinindsimp2  48709  ldepsnlinc  48754  line  48978  rrxline  48980  iscnrm3rlem4  49188