Theorem difeq2d 4063

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4047

This theorem is used by:  difeq12d  4064  iinvdif  5039  otiunsndisj  5492  xpdifid  6158  imain  6626  dffv2  6981  f12dfv  7282  f13dfv  7283  tz7.49  8459  oev2  8535  difsnen  9082  domunsncan  9100  sbthlem2  9111  sbthlem3  9112  sbth  9120  rexdif1en  9180  dif1en  9181  sbthfi  9218  phplem2  9224  unblem2  9289  unblem3  9290  dfac8alem  10112  dfac8a  10113  kmlem9  10241  kmlem11  10243  kmlem12  10244  compsscnvlem  10452  s3iunsndisj  15127  isercolllem3  15840  ruclem13  16416  bitsf1  16622  setsvalg  17350  setsval  17351  setsdm  17354  ismri2dad  17817  mreexmrid  17823  mreexexlemd  17824  gsumvalx  18871  gsumpropd  18873  gsumpropd2lem  18874  gsumress  18877  pmtrfv  19672  gsumval3a  20123  gsumval3  20127  dprdcntz  20230  dprddisj  20231  dprdsn  20258  dprddisj2  20261  dpjval  20278  ablfac1eu  20295  drngprop  21004  subdrgint  21066  lbsind  21361  islbs2  21438  lbsextlem4  21445  lbsextg  21446  frlmlbs  22109  lindfind  22128  lindsind  22129  lindfrn  22133  f1lindf  22134  lindsenlbs  22163  submaval  22902  mdetunilem3  22935  mdetunilem4  22936  mdetunilem9  22941  clsval2  23374  ntrval2  23375  ntrdif  23376  clsdif  23377  cmclsopn  23386  islp  23464  pnrmopn  23667  hauscmplem  23730  bwth  23734  conndisj  23740  cvsunit  25458  bcthlem1  25651  bcth  25656  bcth3  25658  cmmbl  25861  nulmbl2  25863  shftmbl  25865  volsup  25883  mbfimaicc  25958  eldv  26224  ig1pval  26500  tglngval  29020  plngrotlem2  29272  lnssplng  29276  plng3p  29281  tgaaddcpbllem2  29356  axlowdimlem15  29540  axlowdim  29545  nbgr2vtx1edg  29937  nbuhgr2vtx1edgb  29939  nb3grprlem2  29968  uvtxel  29975  uvtxel1  29983  uvtxusgrel  29990  cusgredg  30011  cplgr1v  30017  cplgr3v  30022  usgredgsscusgredg  30046  usgr2pthlem  30355  2wspiundisj  30561  frcond1  30873  frgr1v  30878  nfrgr2v  30879  frgr3v  30882  1vwmgr  30883  3vfriswmgr  30885  3cyclfrgrrn1  30892  n4cyclfrgr  30898  frgrwopreglem4a  30917  supppreima  33332  odpmco  33694  tocycfv  33717  tocycf  33725  tocyc01  33726  cycpm2tr  33727  cycpmconjslem2  33763  cyc3conja  33765  0nellinds  33973  lindssn  33980  extvfval  34211  lbslsat  34295  lindsunlem  34303  ist0cld  34512  sigapildsyslem  34841  carsgclctunlem3  34999  sitgval  35011  ballotlemfval  35169  cplgredgex  35982  cvmscbv  36110  cvmsdisj  36122  cvmsss2  36126  satfv1  36215  satffunlem  36253  satffunlem1lem1  36254  satffunlem2lem1  36256  clsun  37209  lindsadd  38630  poimirlem25  38657  poimirlem26  38658  poimirlem27  38659  cnambfre  38680  watvalN  41144  dnnumch1  44145  aomclem3  44152  aomclem8  44157  safesnsupfilb  44513  dssmapfv2d  45112  dssmapfv3d  45113  dssmapnvod  45114  clsk3nimkb  45134  ntrclscls00  45160  ntrclsiso  45161  ntrclsk3  45164  ntrclsk4  45166  nzprmdif  45397  compne  45518  dvmptfprodlem  47048  fouriercn  47336  meaiininclem  47590  meaiininc  47591  carageniuncllem1  47625  lindslinindsimp2  49669  ldepsnlinc  49714  line  49939  rrxline  49941  iscnrm3rlem4  50151