Theorem difeq2d 4085

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

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

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 3403  df-dif 3914

This theorem is referenced by:  difeq12d  4086  iinvdif  5039  otiunsndisj  5475  xpdifid  6129  imain  6585  dffv2  6938  f12dfv  7230  f13dfv  7231  tz7.49  8390  oev2  8464  difsnen  9000  domunsncan  9018  sbthlem2  9029  sbthlem3  9030  sbth  9038  rexdif1en  9099  rexdif1enOLD  9100  dif1en  9101  dif1enOLD  9103  sbthfi  9140  phplem2  9146  unblem2  9216  unblem3  9217  xpfiOLD  9246  dfac8alem  9958  dfac8a  9959  kmlem9  10088  kmlem11  10090  kmlem12  10091  compsscnvlem  10299  s3iunsndisj  14910  isercolllem3  15609  ruclem13  16186  bitsf1  16392  setsvalg  17112  setsval  17113  setsdm  17116  ismri2dad  17574  mreexmrid  17580  mreexexlemd  17581  gsumvalx  18579  gsumpropd  18581  gsumpropd2lem  18582  gsumress  18585  pmtrfv  19358  gsumval3a  19809  gsumval3  19813  dprdcntz  19916  dprddisj  19917  dprdsn  19944  dprddisj2  19947  dpjval  19964  ablfac1eu  19981  drngprop  20629  subdrgint  20688  lbsind  20963  islbs2  21040  lbsextlem4  21047  lbsextg  21048  frlmlbs  21682  lindfind  21701  lindsind  21702  lindfrn  21706  f1lindf  21707  submaval  22444  mdetunilem3  22477  mdetunilem4  22478  mdetunilem9  22483  clsval2  22913  ntrval2  22914  ntrdif  22915  clsdif  22916  cmclsopn  22925  islp  23003  pnrmopn  23206  hauscmplem  23269  bwth  23273  conndisj  23279  cvsunit  25007  bcthlem1  25200  bcth  25205  bcth3  25207  cmmbl  25411  nulmbl2  25413  shftmbl  25415  volsup  25433  mbfimaicc  25508  eldv  25775  ig1pval  26057  tglngval  28454  axlowdimlem15  28859  axlowdim  28864  nbgr2vtx1edg  29253  nbuhgr2vtx1edgb  29255  nb3grprlem2  29284  uvtxel  29291  uvtxel1  29299  uvtxusgrel  29306  cusgredg  29327  cplgr1v  29333  cplgr3v  29338  usgredgsscusgredg  29363  usgr2pthlem  29666  2wspiundisj  29866  frcond1  30168  frgr1v  30173  nfrgr2v  30174  frgr3v  30177  1vwmgr  30178  3vfriswmgr  30180  3cyclfrgrrn1  30187  n4cyclfrgr  30193  frgrwopreglem4a  30212  supppreima  32587  odpmco  33016  tocycfv  33039  tocycf  33047  tocyc01  33048  cycpm2tr  33049  cycpmconjslem2  33085  cyc3conja  33087  0nellinds  33314  lindssn  33322  lbslsat  33585  lindsunlem  33593  ist0cld  33796  sigapildsyslem  34124  carsgclctunlem3  34284  sitgval  34296  ballotlemfval  34454  cplgredgex  35081  cvmscbv  35218  cvmsdisj  35230  cvmsss2  35234  satfv1  35323  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  clsun  36289  lindsadd  37580  lindsenlbs  37582  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  cnambfre  37635  watvalN  39960  dnnumch1  43006  aomclem3  43018  aomclem8  43023  safesnsupfilb  43380  dssmapfv2d  43980  dssmapfv3d  43981  dssmapnvod  43982  clsk3nimkb  44002  ntrclscls00  44028  ntrclsiso  44029  ntrclsk3  44032  ntrclsk4  44034  nzprmdif  44281  compne  44403  dvmptfprodlem  45915  fouriercn  46203  meaiininclem  46457  meaiininc  46458  carageniuncllem1  46492  lindslinindsimp2  48425  ldepsnlinc  48470  line  48694  rrxline  48696  iscnrm3rlem4  48904