Theorem difeq2d 4080

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  difeq12d  4081  iinvdif  5037  otiunsndisj  5476  xpdifid  6134  imain  6585  dffv2  6937  f12dfv  7229  f13dfv  7230  tz7.49  8386  oev2  8460  difsnen  8999  domunsncan  9017  sbthlem2  9028  sbthlem3  9029  sbth  9037  rexdif1en  9097  dif1en  9098  sbthfi  9135  phplem2  9141  unblem2  9205  unblem3  9206  dfac8alem  9951  dfac8a  9952  kmlem9  10081  kmlem11  10083  kmlem12  10084  compsscnvlem  10292  s3iunsndisj  14903  isercolllem3  15602  ruclem13  16179  bitsf1  16385  setsvalg  17105  setsval  17106  setsdm  17109  ismri2dad  17572  mreexmrid  17578  mreexexlemd  17579  gsumvalx  18613  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  pmtrfv  19393  gsumval3a  19844  gsumval3  19848  dprdcntz  19951  dprddisj  19952  dprdsn  19979  dprddisj2  19982  dpjval  19999  ablfac1eu  20016  drngprop  20689  subdrgint  20748  lbsind  21044  islbs2  21121  lbsextlem4  21128  lbsextg  21129  frlmlbs  21764  lindfind  21783  lindsind  21784  lindfrn  21788  f1lindf  21789  submaval  22537  mdetunilem3  22570  mdetunilem4  22571  mdetunilem9  22576  clsval2  23006  ntrval2  23007  ntrdif  23008  clsdif  23009  cmclsopn  23018  islp  23096  pnrmopn  23299  hauscmplem  23362  bwth  23366  conndisj  23372  cvsunit  25099  bcthlem1  25292  bcth  25297  bcth3  25299  cmmbl  25503  nulmbl2  25505  shftmbl  25507  volsup  25525  mbfimaicc  25600  eldv  25867  ig1pval  26149  tglngval  28635  axlowdimlem15  29041  axlowdim  29046  nbgr2vtx1edg  29435  nbuhgr2vtx1edgb  29437  nb3grprlem2  29466  uvtxel  29473  uvtxel1  29481  uvtxusgrel  29488  cusgredg  29509  cplgr1v  29515  cplgr3v  29520  usgredgsscusgredg  29545  usgr2pthlem  29848  2wspiundisj  30051  frcond1  30353  frgr1v  30358  nfrgr2v  30359  frgr3v  30362  1vwmgr  30363  3vfriswmgr  30365  3cyclfrgrrn1  30372  n4cyclfrgr  30378  frgrwopreglem4a  30397  supppreima  32780  odpmco  33179  tocycfv  33202  tocycf  33210  tocyc01  33211  cycpm2tr  33212  cycpmconjslem2  33248  cyc3conja  33250  0nellinds  33462  lindssn  33470  extvfval  33708  lbslsat  33793  lindsunlem  33801  ist0cld  34010  sigapildsyslem  34338  carsgclctunlem3  34497  sitgval  34509  ballotlemfval  34667  cplgredgex  35334  cvmscbv  35471  cvmsdisj  35483  cvmsss2  35487  satfv1  35576  satffunlem  35614  satffunlem1lem1  35615  satffunlem2lem1  35617  clsun  36541  lindsadd  37861  lindsenlbs  37863  poimirlem25  37893  poimirlem26  37894  poimirlem27  37895  cnambfre  37916  watvalN  40366  dnnumch1  43398  aomclem3  43410  aomclem8  43415  safesnsupfilb  43771  dssmapfv2d  44371  dssmapfv3d  44372  dssmapnvod  44373  clsk3nimkb  44393  ntrclscls00  44419  ntrclsiso  44420  ntrclsk3  44423  ntrclsk4  44425  nzprmdif  44672  compne  44793  dvmptfprodlem  46299  fouriercn  46587  meaiininclem  46841  meaiininc  46842  carageniuncllem1  46876  lindslinindsimp2  48820  ldepsnlinc  48865  line  49089  rrxline  49091  iscnrm3rlem4  49299