Theorem difeq2d 4149

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

Syntax hints:   → wi 4   = wceq 1537   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-dif 3979

This theorem is referenced by:  difeq12d  4150  iinvdif  5103  otiunsndisj  5539  xpdifid  6199  imain  6663  dffv2  7017  f12dfv  7309  f13dfv  7310  tz7.49  8501  oev2  8579  difsnen  9119  domunsncan  9138  sbthlem2  9150  sbthlem3  9151  sbth  9159  rexdif1en  9224  rexdif1enOLD  9225  dif1en  9226  dif1enOLD  9228  sbthfi  9265  phplem2  9271  phplem3OLD  9282  phplem4OLD  9283  unblem2  9357  unblem3  9358  xpfiOLD  9387  dfac8alem  10098  dfac8a  10099  kmlem9  10228  kmlem11  10230  kmlem12  10231  compsscnvlem  10439  s3iunsndisj  15017  isercolllem3  15715  ruclem13  16290  bitsf1  16492  setsvalg  17213  setsval  17214  setsdm  17217  ismri2dad  17695  mreexmrid  17701  mreexexlemd  17702  gsumvalx  18714  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  pmtrfv  19494  gsumval3a  19945  gsumval3  19949  dprdcntz  20052  dprddisj  20053  dprdsn  20080  dprddisj2  20083  dpjval  20100  ablfac1eu  20117  drngprop  20766  subdrgint  20826  lbsind  21102  islbs2  21179  lbsextlem4  21186  lbsextg  21187  frlmlbs  21840  lindfind  21859  lindsind  21860  lindfrn  21864  f1lindf  21865  submaval  22608  mdetunilem3  22641  mdetunilem4  22642  mdetunilem9  22647  clsval2  23079  ntrval2  23080  ntrdif  23081  clsdif  23082  cmclsopn  23091  islp  23169  pnrmopn  23372  hauscmplem  23435  bwth  23439  conndisj  23445  cvsunit  25183  bcthlem1  25377  bcth  25382  bcth3  25384  cmmbl  25588  nulmbl2  25590  shftmbl  25592  volsup  25610  mbfimaicc  25685  eldv  25953  ig1pval  26235  tglngval  28577  axlowdimlem15  28989  axlowdim  28994  nbgr2vtx1edg  29385  nbuhgr2vtx1edgb  29387  nb3grprlem2  29416  uvtxel  29423  uvtxel1  29431  uvtxusgrel  29438  cusgredg  29459  cplgr1v  29465  cplgr3v  29470  usgredgsscusgredg  29495  usgr2pthlem  29799  2wspiundisj  29996  frcond1  30298  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  1vwmgr  30308  3vfriswmgr  30310  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrwopreglem4a  30342  supppreima  32703  odpmco  33079  tocycfv  33102  tocycf  33110  tocyc01  33111  cycpm2tr  33112  cycpmconjslem2  33148  cyc3conja  33150  0nellinds  33363  lindssn  33371  lbslsat  33629  lindsunlem  33637  ist0cld  33779  sigapildsyslem  34125  carsgclctunlem3  34285  sitgval  34297  ballotlemfval  34454  cplgredgex  35088  cvmscbv  35226  cvmsdisj  35238  cvmsss2  35242  satfv1  35331  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  clsun  36294  lindsadd  37573  lindsenlbs  37575  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  cnambfre  37628  watvalN  39950  dnnumch1  43001  aomclem3  43013  aomclem8  43018  safesnsupfilb  43380  dssmapfv2d  43980  dssmapfv3d  43981  dssmapnvod  43982  clsk3nimkb  44002  ntrclscls00  44028  ntrclsiso  44029  ntrclsk3  44032  ntrclsk4  44034  nzprmdif  44288  compne  44410  dvmptfprodlem  45865  fouriercn  46153  meaiininclem  46407  meaiininc  46408  carageniuncllem1  46442  lindslinindsimp2  48192  ldepsnlinc  48237  line  48466  rrxline  48468  iscnrm3rlem4  48623