Theorem difeq2d 3728

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

Syntax hints:   → wi 4   = wceq 1483   ∖ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-rab 2921  df-dif 3577

This theorem is referenced by:  difeq12d  3729  iinvdif  4592  otiunsndisj  4980  xpdifid  5562  imain  5974  dffv2  6271  f12dfv  6529  f13dfv  6530  tz7.49  7540  oev2  7603  difsnen  8042  domunsncan  8060  sbthlem2  8071  sbthlem3  8072  sbth  8080  phplem3  8141  phplem4  8142  unblem2  8213  unblem3  8214  xpfi  8231  dfac8alem  8852  dfac8a  8853  kmlem9  8980  kmlem11  8982  kmlem12  8983  compsscnvlem  9192  s3iunsndisj  13707  isercolllem3  14397  ruclem13  14971  bitsf1  15168  setsvalg  15887  setsval  15888  setsdm  15892  ismri2dad  16297  mreexmrid  16303  mreexexlemd  16304  gsumvalx  17270  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  pmtrfv  17872  gsumval3a  18304  gsumval3  18308  dprdcntz  18407  dprddisj  18408  dprdsn  18435  dprddisj2  18438  dpjval  18455  ablfac1eu  18472  drngprop  18758  lbsind  19080  islbs2  19154  lbsextlem4  19161  lbsextg  19162  frlmlbs  20136  lindfind  20155  lindsind  20156  lindfrn  20160  f1lindf  20161  submaval  20387  mdetunilem3  20420  mdetunilem4  20421  mdetunilem9  20426  clsval2  20854  ntrval2  20855  ntrdif  20856  clsdif  20857  cmclsopn  20866  islp  20944  pnrmopn  21147  hauscmplem  21209  bwth  21213  conndisj  21219  cvsunit  22931  bcthlem1  23121  bcth  23126  bcth3  23128  cmmbl  23302  nulmbl2  23304  shftmbl  23306  volsup  23324  mbfimaicc  23400  eldv  23662  ig1pval  23932  tglngval  25446  axlowdimlem15  25836  axlowdim  25841  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  nb3grprlem2  26283  uvtxael  26288  uvtxael1  26296  uvtxusgrel  26304  cusgredg  26320  cplgr1v  26326  cplgr3v  26331  usgredgsscusgredg  26355  usgr2pthlem  26659  2wspiundisj  26856  frcond1  27130  frgr1v  27135  nfrgr2v  27136  frgr3v  27139  1vwmgr  27140  3vfriswmgr  27142  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrwopreglem4a  27174  sigapildsyslem  30224  carsgclctunlem3  30382  sitgval  30394  ballotlemfval  30551  cvmscbv  31240  cvmsdisj  31252  cvmsss2  31256  clsun  32323  lindsenlbs  33404  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  cnambfre  33458  watvalN  35279  dnnumch1  37614  aomclem3  37626  aomclem8  37631  dssmapfv2d  38312  dssmapfv3d  38313  dssmapnvod  38314  clsk3nimkb  38338  ntrclscls00  38364  ntrclsiso  38365  ntrclsk3  38368  ntrclsk4  38370  nzprmdif  38518  compne  38643  dvmptfprodlem  40159  fouriercn  40449  meaiininclem  40700  meaiininc  40701  carageniuncllem1  40735  lindslinindsimp2  42252  ldepsnlinc  42297