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 1559   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3905

This theorem is referenced by:  difeq12d  4079  iinvdif  5034  otiunsndisj  5486  xpdifid  6149  imain  6601  dffv2  6957  f12dfv  7252  f13dfv  7253  tz7.49  8410  oev2  8486  difsnen  9025  domunsncan  9043  sbthlem2  9054  sbthlem3  9055  sbth  9063  rexdif1en  9123  dif1en  9124  sbthfi  9161  phplem2  9167  unblem2  9231  unblem3  9232  dfac8alem  9979  dfac8a  9980  kmlem9  10109  kmlem11  10111  kmlem12  10112  compsscnvlem  10321  s3iunsndisj  14975  isercolllem3  15685  ruclem13  16265  bitsf1  16471  setsvalg  17193  setsval  17194  setsdm  17197  ismri2dad  17660  mreexmrid  17666  mreexexlemd  17667  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  pmtrfv  19483  gsumval3a  19934  gsumval3  19938  dprdcntz  20041  dprddisj  20042  dprdsn  20069  dprddisj2  20072  dpjval  20089  ablfac1eu  20106  drngprop  20781  subdrgint  20840  lbsind  21135  islbs2  21212  lbsextlem4  21219  lbsextg  21220  frlmlbs  21837  lindfind  21856  lindsind  21857  lindfrn  21861  f1lindf  21862  submaval  22629  mdetunilem3  22662  mdetunilem4  22663  mdetunilem9  22668  clsval2  23098  ntrval2  23099  ntrdif  23100  clsdif  23101  cmclsopn  23110  islp  23188  pnrmopn  23391  hauscmplem  23454  bwth  23458  conndisj  23464  cvsunit  25181  bcthlem1  25374  bcth  25379  bcth3  25381  cmmbl  25584  nulmbl2  25586  shftmbl  25588  volsup  25606  mbfimaicc  25681  eldv  25948  ig1pval  26224  tglngval  28708  axlowdimlem15  29114  axlowdim  29119  nbgr2vtx1edg  29508  nbuhgr2vtx1edgb  29510  nb3grprlem2  29539  uvtxel  29546  uvtxel1  29554  uvtxusgrel  29561  cusgredg  29582  cplgr1v  29588  cplgr3v  29593  usgredgsscusgredg  29617  usgr2pthlem  29920  2wspiundisj  30123  frcond1  30425  frgr1v  30430  nfrgr2v  30431  frgr3v  30434  1vwmgr  30435  3vfriswmgr  30437  3cyclfrgrrn1  30444  n4cyclfrgr  30450  frgrwopreglem4a  30469  supppreima  32854  odpmco  33227  tocycfv  33250  tocycf  33258  tocyc01  33259  cycpm2tr  33260  cycpmconjslem2  33296  cyc3conja  33298  0nellinds  33517  lindssn  33525  extvfval  33790  lbslsat  33874  lindsunlem  33882  ist0cld  34091  sigapildsyslem  34419  carsgclctunlem3  34578  sitgval  34590  ballotlemfval  34748  cplgredgex  35432  cvmscbv  35569  cvmsdisj  35581  cvmsss2  35585  satfv1  35674  satffunlem  35712  satffunlem1lem1  35713  satffunlem2lem1  35715  clsun  36649  lindsadd  38073  lindsenlbs  38075  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  cnambfre  38128  watvalN  40578  dnnumch1  43582  aomclem3  43594  aomclem8  43599  safesnsupfilb  43955  dssmapfv2d  44555  dssmapfv3d  44556  dssmapnvod  44557  clsk3nimkb  44577  ntrclscls00  44603  ntrclsiso  44604  ntrclsk3  44607  ntrclsk4  44609  nzprmdif  44856  compne  44977  dvmptfprodlem  46479  fouriercn  46767  meaiininclem  47021  meaiininc  47022  carageniuncllem1  47056  lindslinindsimp2  49046  ldepsnlinc  49091  line  49315  rrxline  49317  iscnrm3rlem4  49525