Theorem difeq2d 4135

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

Syntax hints:   → wi 4   = wceq 1536   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-dif 3965

This theorem is referenced by:  difeq12d  4136  iinvdif  5084  otiunsndisj  5529  xpdifid  6189  imain  6652  dffv2  7003  f12dfv  7292  f13dfv  7293  tz7.49  8483  oev2  8559  difsnen  9091  domunsncan  9110  sbthlem2  9122  sbthlem3  9123  sbth  9131  rexdif1en  9196  rexdif1enOLD  9197  dif1en  9198  dif1enOLD  9200  sbthfi  9236  phplem2  9242  phplem3OLD  9253  phplem4OLD  9254  unblem2  9326  unblem3  9327  xpfiOLD  9356  dfac8alem  10066  dfac8a  10067  kmlem9  10196  kmlem11  10198  kmlem12  10199  compsscnvlem  10407  s3iunsndisj  15003  isercolllem3  15699  ruclem13  16274  bitsf1  16479  setsvalg  17199  setsval  17200  setsdm  17203  ismri2dad  17681  mreexmrid  17687  mreexexlemd  17688  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  pmtrfv  19484  gsumval3a  19935  gsumval3  19939  dprdcntz  20042  dprddisj  20043  dprdsn  20070  dprddisj2  20073  dpjval  20090  ablfac1eu  20107  drngprop  20760  subdrgint  20820  lbsind  21096  islbs2  21173  lbsextlem4  21180  lbsextg  21181  frlmlbs  21834  lindfind  21853  lindsind  21854  lindfrn  21858  f1lindf  21859  submaval  22602  mdetunilem3  22635  mdetunilem4  22636  mdetunilem9  22641  clsval2  23073  ntrval2  23074  ntrdif  23075  clsdif  23076  cmclsopn  23085  islp  23163  pnrmopn  23366  hauscmplem  23429  bwth  23433  conndisj  23439  cvsunit  25177  bcthlem1  25371  bcth  25376  bcth3  25378  cmmbl  25582  nulmbl2  25584  shftmbl  25586  volsup  25604  mbfimaicc  25679  eldv  25947  ig1pval  26229  tglngval  28573  axlowdimlem15  28985  axlowdim  28990  nbgr2vtx1edg  29381  nbuhgr2vtx1edgb  29383  nb3grprlem2  29412  uvtxel  29419  uvtxel1  29427  uvtxusgrel  29434  cusgredg  29455  cplgr1v  29461  cplgr3v  29466  usgredgsscusgredg  29491  usgr2pthlem  29795  2wspiundisj  29992  frcond1  30294  frgr1v  30299  nfrgr2v  30300  frgr3v  30303  1vwmgr  30304  3vfriswmgr  30306  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrwopreglem4a  30338  supppreima  32705  odpmco  33088  tocycfv  33111  tocycf  33119  tocyc01  33120  cycpm2tr  33121  cycpmconjslem2  33157  cyc3conja  33159  0nellinds  33377  lindssn  33385  lbslsat  33643  lindsunlem  33651  ist0cld  33793  sigapildsyslem  34141  carsgclctunlem3  34301  sitgval  34313  ballotlemfval  34470  cplgredgex  35104  cvmscbv  35242  cvmsdisj  35254  cvmsss2  35258  satfv1  35347  satffunlem  35385  satffunlem1lem1  35386  satffunlem2lem1  35388  clsun  36310  lindsadd  37599  lindsenlbs  37601  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  cnambfre  37654  watvalN  39975  dnnumch1  43032  aomclem3  43044  aomclem8  43049  safesnsupfilb  43407  dssmapfv2d  44007  dssmapfv3d  44008  dssmapnvod  44009  clsk3nimkb  44029  ntrclscls00  44055  ntrclsiso  44056  ntrclsk3  44059  ntrclsk4  44061  nzprmdif  44314  compne  44436  dvmptfprodlem  45899  fouriercn  46187  meaiininclem  46441  meaiininc  46442  carageniuncllem1  46476  lindslinindsimp2  48308  ldepsnlinc  48353  line  48581  rrxline  48583  iscnrm3rlem4  48739