Theorem difeq2d 4071

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

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-dif 3900

This theorem is referenced by:  difeq12d  4072  iinvdif  5023  otiunsndisj  5455  xpdifid  6110  imain  6561  dffv2  6912  f12dfv  7202  f13dfv  7203  tz7.49  8359  oev2  8433  difsnen  8967  domunsncan  8985  sbthlem2  8996  sbthlem3  8997  sbth  9005  rexdif1en  9065  dif1en  9066  sbthfi  9103  phplem2  9109  unblem2  9172  unblem3  9173  dfac8alem  9915  dfac8a  9916  kmlem9  10045  kmlem11  10047  kmlem12  10048  compsscnvlem  10256  s3iunsndisj  14870  isercolllem3  15569  ruclem13  16146  bitsf1  16352  setsvalg  17072  setsval  17073  setsdm  17076  ismri2dad  17538  mreexmrid  17544  mreexexlemd  17545  gsumvalx  18579  gsumpropd  18581  gsumpropd2lem  18582  gsumress  18585  pmtrfv  19359  gsumval3a  19810  gsumval3  19814  dprdcntz  19917  dprddisj  19918  dprdsn  19945  dprddisj2  19948  dpjval  19965  ablfac1eu  19982  drngprop  20654  subdrgint  20713  lbsind  21009  islbs2  21086  lbsextlem4  21093  lbsextg  21094  frlmlbs  21729  lindfind  21748  lindsind  21749  lindfrn  21753  f1lindf  21754  submaval  22491  mdetunilem3  22524  mdetunilem4  22525  mdetunilem9  22530  clsval2  22960  ntrval2  22961  ntrdif  22962  clsdif  22963  cmclsopn  22972  islp  23050  pnrmopn  23253  hauscmplem  23316  bwth  23320  conndisj  23326  cvsunit  25053  bcthlem1  25246  bcth  25251  bcth3  25253  cmmbl  25457  nulmbl2  25459  shftmbl  25461  volsup  25479  mbfimaicc  25554  eldv  25821  ig1pval  26103  tglngval  28524  axlowdimlem15  28929  axlowdim  28934  nbgr2vtx1edg  29323  nbuhgr2vtx1edgb  29325  nb3grprlem2  29354  uvtxel  29361  uvtxel1  29369  uvtxusgrel  29376  cusgredg  29397  cplgr1v  29403  cplgr3v  29408  usgredgsscusgredg  29433  usgr2pthlem  29736  2wspiundisj  29936  frcond1  30238  frgr1v  30243  nfrgr2v  30244  frgr3v  30247  1vwmgr  30248  3vfriswmgr  30250  3cyclfrgrrn1  30257  n4cyclfrgr  30263  frgrwopreglem4a  30282  supppreima  32664  odpmco  33047  tocycfv  33070  tocycf  33078  tocyc01  33079  cycpm2tr  33080  cycpmconjslem2  33116  cyc3conja  33118  0nellinds  33327  lindssn  33335  lbslsat  33621  lindsunlem  33629  ist0cld  33838  sigapildsyslem  34166  carsgclctunlem3  34325  sitgval  34337  ballotlemfval  34495  cplgredgex  35157  cvmscbv  35294  cvmsdisj  35306  cvmsss2  35310  satfv1  35399  satffunlem  35437  satffunlem1lem1  35438  satffunlem2lem1  35440  clsun  36362  lindsadd  37653  lindsenlbs  37655  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  cnambfre  37708  watvalN  40032  dnnumch1  43077  aomclem3  43089  aomclem8  43094  safesnsupfilb  43451  dssmapfv2d  44051  dssmapfv3d  44052  dssmapnvod  44053  clsk3nimkb  44073  ntrclscls00  44099  ntrclsiso  44100  ntrclsk3  44103  ntrclsk4  44105  nzprmdif  44352  compne  44473  dvmptfprodlem  45982  fouriercn  46270  meaiininclem  46524  meaiininc  46525  carageniuncllem1  46559  lindslinindsimp2  48495  ldepsnlinc  48540  line  48764  rrxline  48766  iscnrm3rlem4  48974