Theorem difeq2d 4066

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3886

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  difeq12d  4067  iinvdif  5022  otiunsndisj  5474  xpdifid  6132  imain  6583  dffv2  6935  f12dfv  7228  f13dfv  7229  tz7.49  8384  oev2  8458  difsnen  8997  domunsncan  9015  sbthlem2  9026  sbthlem3  9027  sbth  9035  rexdif1en  9095  dif1en  9096  sbthfi  9133  phplem2  9139  unblem2  9203  unblem3  9204  dfac8alem  9951  dfac8a  9952  kmlem9  10081  kmlem11  10083  kmlem12  10084  compsscnvlem  10292  s3iunsndisj  14930  isercolllem3  15629  ruclem13  16209  bitsf1  16415  setsvalg  17136  setsval  17137  setsdm  17140  ismri2dad  17603  mreexmrid  17609  mreexexlemd  17610  gsumvalx  18644  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  pmtrfv  19427  gsumval3a  19878  gsumval3  19882  dprdcntz  19985  dprddisj  19986  dprdsn  20013  dprddisj2  20016  dpjval  20033  ablfac1eu  20050  drngprop  20721  subdrgint  20780  lbsind  21075  islbs2  21152  lbsextlem4  21159  lbsextg  21160  frlmlbs  21777  lindfind  21796  lindsind  21797  lindfrn  21801  f1lindf  21802  submaval  22546  mdetunilem3  22579  mdetunilem4  22580  mdetunilem9  22585  clsval2  23015  ntrval2  23016  ntrdif  23017  clsdif  23018  cmclsopn  23027  islp  23105  pnrmopn  23308  hauscmplem  23371  bwth  23375  conndisj  23381  cvsunit  25098  bcthlem1  25291  bcth  25296  bcth3  25298  cmmbl  25501  nulmbl2  25503  shftmbl  25505  volsup  25523  mbfimaicc  25598  eldv  25865  ig1pval  26141  tglngval  28619  axlowdimlem15  29025  axlowdim  29030  nbgr2vtx1edg  29419  nbuhgr2vtx1edgb  29421  nb3grprlem2  29450  uvtxel  29457  uvtxel1  29465  uvtxusgrel  29472  cusgredg  29493  cplgr1v  29499  cplgr3v  29504  usgredgsscusgredg  29528  usgr2pthlem  29831  2wspiundisj  30034  frcond1  30336  frgr1v  30341  nfrgr2v  30342  frgr3v  30345  1vwmgr  30346  3vfriswmgr  30348  3cyclfrgrrn1  30355  n4cyclfrgr  30361  frgrwopreglem4a  30380  supppreima  32764  odpmco  33147  tocycfv  33170  tocycf  33178  tocyc01  33179  cycpm2tr  33180  cycpmconjslem2  33216  cyc3conja  33218  0nellinds  33430  lindssn  33438  extvfval  33676  lbslsat  33760  lindsunlem  33768  ist0cld  33977  sigapildsyslem  34305  carsgclctunlem3  34464  sitgval  34476  ballotlemfval  34634  cplgredgex  35303  cvmscbv  35440  cvmsdisj  35452  cvmsss2  35456  satfv1  35545  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  clsun  36510  lindsadd  37934  lindsenlbs  37936  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  cnambfre  37989  watvalN  40439  dnnumch1  43472  aomclem3  43484  aomclem8  43489  safesnsupfilb  43845  dssmapfv2d  44445  dssmapfv3d  44446  dssmapnvod  44447  clsk3nimkb  44467  ntrclscls00  44493  ntrclsiso  44494  ntrclsk3  44497  ntrclsk4  44499  nzprmdif  44746  compne  44867  dvmptfprodlem  46372  fouriercn  46660  meaiininclem  46914  meaiininc  46915  carageniuncllem1  46949  lindslinindsimp2  48939  ldepsnlinc  48984  line  49208  rrxline  49210  iscnrm3rlem4  49418