Theorem difeq2d 4092

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920

This theorem is referenced by:  difeq12d  4093  iinvdif  5047  otiunsndisj  5483  xpdifid  6144  imain  6604  dffv2  6959  f12dfv  7251  f13dfv  7252  tz7.49  8416  oev2  8490  difsnen  9027  domunsncan  9046  sbthlem2  9058  sbthlem3  9059  sbth  9067  rexdif1en  9128  rexdif1enOLD  9129  dif1en  9130  dif1enOLD  9132  sbthfi  9169  phplem2  9175  unblem2  9247  unblem3  9248  xpfiOLD  9277  dfac8alem  9989  dfac8a  9990  kmlem9  10119  kmlem11  10121  kmlem12  10122  compsscnvlem  10330  s3iunsndisj  14941  isercolllem3  15640  ruclem13  16217  bitsf1  16423  setsvalg  17143  setsval  17144  setsdm  17147  ismri2dad  17605  mreexmrid  17611  mreexexlemd  17612  gsumvalx  18610  gsumpropd  18612  gsumpropd2lem  18613  gsumress  18616  pmtrfv  19389  gsumval3a  19840  gsumval3  19844  dprdcntz  19947  dprddisj  19948  dprdsn  19975  dprddisj2  19978  dpjval  19995  ablfac1eu  20012  drngprop  20660  subdrgint  20719  lbsind  20994  islbs2  21071  lbsextlem4  21078  lbsextg  21079  frlmlbs  21713  lindfind  21732  lindsind  21733  lindfrn  21737  f1lindf  21738  submaval  22475  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  clsval2  22944  ntrval2  22945  ntrdif  22946  clsdif  22947  cmclsopn  22956  islp  23034  pnrmopn  23237  hauscmplem  23300  bwth  23304  conndisj  23310  cvsunit  25038  bcthlem1  25231  bcth  25236  bcth3  25238  cmmbl  25442  nulmbl2  25444  shftmbl  25446  volsup  25464  mbfimaicc  25539  eldv  25806  ig1pval  26088  tglngval  28485  axlowdimlem15  28890  axlowdim  28895  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  nb3grprlem2  29315  uvtxel  29322  uvtxel1  29330  uvtxusgrel  29337  cusgredg  29358  cplgr1v  29364  cplgr3v  29369  usgredgsscusgredg  29394  usgr2pthlem  29700  2wspiundisj  29900  frcond1  30202  frgr1v  30207  nfrgr2v  30208  frgr3v  30211  1vwmgr  30212  3vfriswmgr  30214  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrwopreglem4a  30246  supppreima  32621  odpmco  33050  tocycfv  33073  tocycf  33081  tocyc01  33082  cycpm2tr  33083  cycpmconjslem2  33119  cyc3conja  33121  0nellinds  33348  lindssn  33356  lbslsat  33619  lindsunlem  33627  ist0cld  33830  sigapildsyslem  34158  carsgclctunlem3  34318  sitgval  34330  ballotlemfval  34488  cplgredgex  35115  cvmscbv  35252  cvmsdisj  35264  cvmsss2  35268  satfv1  35357  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  clsun  36323  lindsadd  37614  lindsenlbs  37616  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  cnambfre  37669  watvalN  39994  dnnumch1  43040  aomclem3  43052  aomclem8  43057  safesnsupfilb  43414  dssmapfv2d  44014  dssmapfv3d  44015  dssmapnvod  44016  clsk3nimkb  44036  ntrclscls00  44062  ntrclsiso  44063  ntrclsk3  44066  ntrclsk4  44068  nzprmdif  44315  compne  44437  dvmptfprodlem  45949  fouriercn  46237  meaiininclem  46491  meaiininc  46492  carageniuncllem1  46526  lindslinindsimp2  48456  ldepsnlinc  48501  line  48725  rrxline  48727  iscnrm3rlem4  48935