Theorem difeq2d 4118

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-dif 3947

This theorem is referenced by:  difeq12d  4119  iinvdif  5076  otiunsndisj  5513  xpdifid  6156  imain  6622  dffv2  6972  f12dfv  7255  f13dfv  7256  tz7.49  8427  oev2  8505  difsnen  9036  domunsncan  9055  sbthlem2  9067  sbthlem3  9068  sbth  9076  rexdif1en  9141  rexdif1enOLD  9142  dif1en  9143  dif1enOLD  9145  sbthfi  9185  phplem2  9191  phplem3OLD  9202  phplem4OLD  9203  unblem2  9279  unblem3  9280  xpfiOLD  9301  dfac8alem  10006  dfac8a  10007  kmlem9  10135  kmlem11  10137  kmlem12  10138  compsscnvlem  10347  s3iunsndisj  14897  isercolllem3  15595  ruclem13  16167  bitsf1  16369  setsvalg  17081  setsval  17082  setsdm  17085  ismri2dad  17563  mreexmrid  17569  mreexexlemd  17570  gsumvalx  18577  gsumpropd  18579  gsumpropd2lem  18580  gsumress  18583  pmtrfv  19284  gsumval3a  19730  gsumval3  19734  dprdcntz  19837  dprddisj  19838  dprdsn  19865  dprddisj2  19868  dpjval  19885  ablfac1eu  19902  drngprop  20279  subdrgint  20368  lbsind  20640  islbs2  20716  lbsextlem4  20723  lbsextg  20724  frlmlbs  21285  lindfind  21304  lindsind  21305  lindfrn  21309  f1lindf  21310  submaval  22012  mdetunilem3  22045  mdetunilem4  22046  mdetunilem9  22051  clsval2  22483  ntrval2  22484  ntrdif  22485  clsdif  22486  cmclsopn  22495  islp  22573  pnrmopn  22776  hauscmplem  22839  bwth  22843  conndisj  22849  cvsunit  24576  bcthlem1  24770  bcth  24775  bcth3  24777  cmmbl  24980  nulmbl2  24982  shftmbl  24984  volsup  25002  mbfimaicc  25077  eldv  25344  ig1pval  25619  tglngval  27667  axlowdimlem15  28079  axlowdim  28084  nbgr2vtx1edg  28472  nbuhgr2vtx1edgb  28474  nb3grprlem2  28503  uvtxel  28510  uvtxel1  28518  uvtxusgrel  28525  cusgredg  28546  cplgr1v  28552  cplgr3v  28557  usgredgsscusgredg  28581  usgr2pthlem  28885  2wspiundisj  29082  frcond1  29384  frgr1v  29389  nfrgr2v  29390  frgr3v  29393  1vwmgr  29394  3vfriswmgr  29396  3cyclfrgrrn1  29403  n4cyclfrgr  29409  frgrwopreglem4a  29428  supppreima  31784  odpmco  32118  tocycfv  32139  tocycf  32147  tocyc01  32148  cycpm2tr  32149  cycpmconjslem2  32185  cyc3conja  32187  0nellinds  32345  lindssn  32352  lbslsat  32539  lindsunlem  32547  ist0cld  32644  sigapildsyslem  32990  carsgclctunlem3  33150  sitgval  33162  ballotlemfval  33319  cplgredgex  33942  cvmscbv  34080  cvmsdisj  34092  cvmsss2  34096  satfv1  34185  satffunlem  34223  satffunlem1lem1  34224  satffunlem2lem1  34226  clsun  35017  lindsadd  36285  lindsenlbs  36287  poimirlem25  36317  poimirlem26  36318  poimirlem27  36319  cnambfre  36340  watvalN  38669  dnnumch1  41557  aomclem3  41569  aomclem8  41574  safesnsupfilb  41940  dssmapfv2d  42540  dssmapfv3d  42541  dssmapnvod  42542  clsk3nimkb  42562  ntrclscls00  42588  ntrclsiso  42589  ntrclsk3  42592  ntrclsk4  42594  nzprmdif  42849  compne  42971  dvmptfprodlem  44433  fouriercn  44721  meaiininclem  44975  meaiininc  44976  carageniuncllem1  45010  lindslinindsimp2  46792  ldepsnlinc  46837  line  47066  rrxline  47068  iscnrm3rlem4  47224