Theorem difeq2d 4057

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

Syntax hints:   → wi 4   = wceq 1547   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-dif 3886

This theorem is referenced by:  difeq12d  4058  iinvdif  5009  otiunsndisj  5461  xpdifid  6119  imain  6570  dffv2  6922  f12dfv  7217  f13dfv  7218  tz7.49  8374  oev2  8448  difsnen  8987  domunsncan  9005  sbthlem2  9016  sbthlem3  9017  sbth  9025  rexdif1en  9085  dif1en  9086  sbthfi  9123  phplem2  9129  unblem2  9193  unblem3  9194  dfac8alem  9942  dfac8a  9943  kmlem9  10072  kmlem11  10074  kmlem12  10075  compsscnvlem  10283  s3iunsndisj  14921  isercolllem3  15620  ruclem13  16200  bitsf1  16406  setsvalg  17127  setsval  17128  setsdm  17131  ismri2dad  17594  mreexmrid  17600  mreexexlemd  17601  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  pmtrfv  19418  gsumval3a  19869  gsumval3  19873  dprdcntz  19976  dprddisj  19977  dprdsn  20004  dprddisj2  20007  dpjval  20024  ablfac1eu  20041  drngprop  20716  subdrgint  20775  lbsind  21070  islbs2  21147  lbsextlem4  21154  lbsextg  21155  frlmlbs  21772  lindfind  21791  lindsind  21792  lindfrn  21796  f1lindf  21797  submaval  22564  mdetunilem3  22597  mdetunilem4  22598  mdetunilem9  22603  clsval2  23033  ntrval2  23034  ntrdif  23035  clsdif  23036  cmclsopn  23045  islp  23123  pnrmopn  23326  hauscmplem  23389  bwth  23393  conndisj  23399  cvsunit  25116  bcthlem1  25309  bcth  25314  bcth3  25316  cmmbl  25519  nulmbl2  25521  shftmbl  25523  volsup  25541  mbfimaicc  25616  eldv  25883  ig1pval  26159  tglngval  28637  axlowdimlem15  29043  axlowdim  29048  nbgr2vtx1edg  29437  nbuhgr2vtx1edgb  29439  nb3grprlem2  29468  uvtxel  29475  uvtxel1  29483  uvtxusgrel  29490  cusgredg  29511  cplgr1v  29517  cplgr3v  29522  usgredgsscusgredg  29546  usgr2pthlem  29849  2wspiundisj  30052  frcond1  30354  frgr1v  30359  nfrgr2v  30360  frgr3v  30363  1vwmgr  30364  3vfriswmgr  30366  3cyclfrgrrn1  30373  n4cyclfrgr  30379  frgrwopreglem4a  30398  supppreima  32783  odpmco  33167  tocycfv  33190  tocycf  33198  tocyc01  33199  cycpm2tr  33200  cycpmconjslem2  33236  cyc3conja  33238  0nellinds  33453  lindssn  33461  extvfval  33716  lbslsat  33800  lindsunlem  33808  ist0cld  34017  sigapildsyslem  34345  carsgclctunlem3  34504  sitgval  34516  ballotlemfval  34674  cplgredgex  35349  cvmscbv  35486  cvmsdisj  35498  cvmsss2  35502  satfv1  35591  satffunlem  35629  satffunlem1lem1  35630  satffunlem2lem1  35632  clsun  36556  lindsadd  37980  lindsenlbs  37982  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  cnambfre  38035  watvalN  40485  dnnumch1  43489  aomclem3  43501  aomclem8  43506  safesnsupfilb  43862  dssmapfv2d  44462  dssmapfv3d  44463  dssmapnvod  44464  clsk3nimkb  44484  ntrclscls00  44510  ntrclsiso  44511  ntrclsk3  44514  ntrclsk4  44516  nzprmdif  44763  compne  44884  dvmptfprodlem  46387  fouriercn  46675  meaiininclem  46929  meaiininc  46930  carageniuncllem1  46964  lindslinindsimp2  48954  ldepsnlinc  48999  line  49223  rrxline  49225  iscnrm3rlem4  49433