Theorem difeq2d 3690

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

Syntax hints:   → wi 4   = wceq 1475   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-rab 2905  df-dif 3543

This theorem is referenced by:  difeq12d  3691  iinvdif  4528  otiunsndisj  4905  xpdifid  5481  imain  5888  dffv2  6181  f12dfv  6429  f13dfv  6430  tz7.49  7427  oev2  7490  difsnen  7927  domunsncan  7945  sbthlem2  7956  sbthlem3  7957  sbth  7965  phplem3  8026  phplem4  8027  unblem2  8098  unblem3  8099  xpfi  8116  dfac8alem  8735  dfac8a  8736  kmlem9  8863  kmlem11  8865  kmlem12  8866  compsscnvlem  9075  s3iunsndisj  13555  isercolllem3  14245  ruclem13  14810  bitsf1  15006  setsvalg  15719  setsval  15720  setsdm  15724  ismri2dad  16120  mreexmrid  16126  mreexexlemd  16127  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  pmtrfv  17695  gsumval3a  18127  gsumval3  18131  dprdcntz  18230  dprddisj  18231  dprdsn  18258  dprddisj2  18261  dpjval  18278  ablfac1eu  18295  drngprop  18581  lbsind  18901  islbs2  18975  lbsextlem4  18982  lbsextg  18983  frlmlbs  19955  lindfind  19974  lindsind  19975  lindfrn  19979  f1lindf  19980  submaval  20206  mdetunilem3  20239  mdetunilem4  20240  mdetunilem9  20245  clsval2  20664  ntrval2  20665  ntrdif  20666  clsdif  20667  cmclsopn  20676  islp  20754  pnrmopn  20957  hauscmplem  21019  bwth  21023  conndisj  21029  cvsunit  22739  bcthlem1  22929  bcth  22934  bcth3  22936  cmmbl  23109  nulmbl2  23111  shftmbl  23113  volsup  23131  mbfimaicc  23206  eldv  23468  ig1pval  23736  tglngval  25246  axlowdimlem15  25636  axlowdim  25641  nb3graprlem2  25981  cusgrarn  25988  cusgra1v  25990  cusgra2v  25991  cusgra3v  25993  usgrasscusgra  26011  sizeusglecusglem1  26012  uvtxel  26017  cusgrauvtxb  26024  frgraunss  26522  frgra1v  26525  frgra2v  26526  frgra3v  26529  1vwmgra  26530  3vfriswmgra  26532  3cyclfrgrarn1  26539  n4cyclfrgra  26545  frgrancvvdeqlem4  26560  frgrawopreglem4  26574  frgraregorufr0  26579  2spotiundisj  26589  sigapildsyslem  29551  carsgclctunlem3  29709  sitgval  29721  ballotlemfval  29878  cvmscbv  30494  cvmsdisj  30506  cvmsss2  30510  clsun  31493  lindsenlbs  32574  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  cnambfre  32628  watvalN  34297  dnnumch1  36632  aomclem3  36644  aomclem8  36649  dssmapfv2d  37332  dssmapfv3d  37333  dssmapnvod  37334  clsk3nimkb  37358  ntrclscls00  37384  ntrclsiso  37385  ntrclsk3  37388  ntrclsk4  37390  nzprmdif  37540  dvmptfprodlem  38834  fouriercn  39125  meaiininclem  39376  meaiininc  39377  carageniuncllem1  39411  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  nb3grprlem2  40609  uvtxael  40614  uvtxael1  40622  uvtxusgrel  40630  cusgredg  40646  cplgr1v  40652  cplgr3v  40657  usgredgsscusgredg  40675  usgr2pthlem  40969  2wspiundisj  41166  frcond1  41438  frgr1v  41441  nfrgr2v  41442  frgr3v  41445  1vwmgr  41446  3vfriswmgr  41448  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrncvvdeqlem4  41472  frgrwopreglem4  41484  frgrregorufr0  41489  lindslinindsimp2  42046  ldepsnlinc  42091