Theorem difeq2d 4079

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-dif 3908

This theorem is referenced by:  difeq12d  4080  iinvdif  5032  otiunsndisj  5467  xpdifid  6121  imain  6571  dffv2  6922  f12dfv  7214  f13dfv  7215  tz7.49  8374  oev2  8448  difsnen  8983  domunsncan  9001  sbthlem2  9012  sbthlem3  9013  sbth  9021  rexdif1en  9082  rexdif1enOLD  9083  dif1en  9084  dif1enOLD  9086  sbthfi  9123  phplem2  9129  unblem2  9198  unblem3  9199  xpfiOLD  9228  dfac8alem  9942  dfac8a  9943  kmlem9  10072  kmlem11  10074  kmlem12  10075  compsscnvlem  10283  s3iunsndisj  14893  isercolllem3  15592  ruclem13  16169  bitsf1  16375  setsvalg  17095  setsval  17096  setsdm  17099  ismri2dad  17561  mreexmrid  17567  mreexexlemd  17568  gsumvalx  18568  gsumpropd  18570  gsumpropd2lem  18571  gsumress  18574  pmtrfv  19349  gsumval3a  19800  gsumval3  19804  dprdcntz  19907  dprddisj  19908  dprdsn  19935  dprddisj2  19938  dpjval  19955  ablfac1eu  19972  drngprop  20647  subdrgint  20706  lbsind  21002  islbs2  21079  lbsextlem4  21086  lbsextg  21087  frlmlbs  21722  lindfind  21741  lindsind  21742  lindfrn  21746  f1lindf  21747  submaval  22484  mdetunilem3  22517  mdetunilem4  22518  mdetunilem9  22523  clsval2  22953  ntrval2  22954  ntrdif  22955  clsdif  22956  cmclsopn  22965  islp  23043  pnrmopn  23246  hauscmplem  23309  bwth  23313  conndisj  23319  cvsunit  25047  bcthlem1  25240  bcth  25245  bcth3  25247  cmmbl  25451  nulmbl2  25453  shftmbl  25455  volsup  25473  mbfimaicc  25548  eldv  25815  ig1pval  26097  tglngval  28514  axlowdimlem15  28919  axlowdim  28924  nbgr2vtx1edg  29313  nbuhgr2vtx1edgb  29315  nb3grprlem2  29344  uvtxel  29351  uvtxel1  29359  uvtxusgrel  29366  cusgredg  29387  cplgr1v  29393  cplgr3v  29398  usgredgsscusgredg  29423  usgr2pthlem  29726  2wspiundisj  29926  frcond1  30228  frgr1v  30233  nfrgr2v  30234  frgr3v  30237  1vwmgr  30238  3vfriswmgr  30240  3cyclfrgrrn1  30247  n4cyclfrgr  30253  frgrwopreglem4a  30272  supppreima  32647  odpmco  33041  tocycfv  33064  tocycf  33072  tocyc01  33073  cycpm2tr  33074  cycpmconjslem2  33110  cyc3conja  33112  0nellinds  33320  lindssn  33328  lbslsat  33591  lindsunlem  33599  ist0cld  33802  sigapildsyslem  34130  carsgclctunlem3  34290  sitgval  34302  ballotlemfval  34460  cplgredgex  35096  cvmscbv  35233  cvmsdisj  35245  cvmsss2  35249  satfv1  35338  satffunlem  35376  satffunlem1lem1  35377  satffunlem2lem1  35379  clsun  36304  lindsadd  37595  lindsenlbs  37597  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  cnambfre  37650  watvalN  39975  dnnumch1  43020  aomclem3  43032  aomclem8  43037  safesnsupfilb  43394  dssmapfv2d  43994  dssmapfv3d  43995  dssmapnvod  43996  clsk3nimkb  44016  ntrclscls00  44042  ntrclsiso  44043  ntrclsk3  44046  ntrclsk4  44048  nzprmdif  44295  compne  44417  dvmptfprodlem  45929  fouriercn  46217  meaiininclem  46471  meaiininc  46472  carageniuncllem1  46506  lindslinindsimp2  48452  ldepsnlinc  48497  line  48721  rrxline  48723  iscnrm3rlem4  48931