Theorem difeq2d 4121

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3944

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-dif 3950

This theorem is referenced by:  difeq12d  4122  iinvdif  5082  otiunsndisj  5519  xpdifid  6166  imain  6632  dffv2  6985  f12dfv  7273  f13dfv  7274  tz7.49  8447  oev2  8525  difsnen  9055  domunsncan  9074  sbthlem2  9086  sbthlem3  9087  sbth  9095  rexdif1en  9160  rexdif1enOLD  9161  dif1en  9162  dif1enOLD  9164  sbthfi  9204  phplem2  9210  phplem3OLD  9221  phplem4OLD  9222  unblem2  9298  unblem3  9299  xpfiOLD  9320  dfac8alem  10026  dfac8a  10027  kmlem9  10155  kmlem11  10157  kmlem12  10158  compsscnvlem  10367  s3iunsndisj  14919  isercolllem3  15617  ruclem13  16189  bitsf1  16391  setsvalg  17103  setsval  17104  setsdm  17107  ismri2dad  17585  mreexmrid  17591  mreexexlemd  17592  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  pmtrfv  19361  gsumval3a  19812  gsumval3  19816  dprdcntz  19919  dprddisj  19920  dprdsn  19947  dprddisj2  19950  dpjval  19967  ablfac1eu  19984  drngprop  20515  subdrgint  20562  lbsind  20835  islbs2  20912  lbsextlem4  20919  lbsextg  20920  frlmlbs  21571  lindfind  21590  lindsind  21591  lindfrn  21595  f1lindf  21596  submaval  22303  mdetunilem3  22336  mdetunilem4  22337  mdetunilem9  22342  clsval2  22774  ntrval2  22775  ntrdif  22776  clsdif  22777  cmclsopn  22786  islp  22864  pnrmopn  23067  hauscmplem  23130  bwth  23134  conndisj  23140  cvsunit  24878  bcthlem1  25072  bcth  25077  bcth3  25079  cmmbl  25283  nulmbl2  25285  shftmbl  25287  volsup  25305  mbfimaicc  25380  eldv  25647  ig1pval  25925  tglngval  28069  axlowdimlem15  28481  axlowdim  28486  nbgr2vtx1edg  28874  nbuhgr2vtx1edgb  28876  nb3grprlem2  28905  uvtxel  28912  uvtxel1  28920  uvtxusgrel  28927  cusgredg  28948  cplgr1v  28954  cplgr3v  28959  usgredgsscusgredg  28983  usgr2pthlem  29287  2wspiundisj  29484  frcond1  29786  frgr1v  29791  nfrgr2v  29792  frgr3v  29795  1vwmgr  29796  3vfriswmgr  29798  3cyclfrgrrn1  29805  n4cyclfrgr  29811  frgrwopreglem4a  29830  supppreima  32180  odpmco  32517  tocycfv  32538  tocycf  32546  tocyc01  32547  cycpm2tr  32548  cycpmconjslem2  32584  cyc3conja  32586  0nellinds  32757  lindssn  32768  lbslsat  32989  lindsunlem  32997  ist0cld  33111  sigapildsyslem  33457  carsgclctunlem3  33617  sitgval  33629  ballotlemfval  33786  cplgredgex  34409  cvmscbv  34547  cvmsdisj  34559  cvmsss2  34563  satfv1  34652  satffunlem  34690  satffunlem1lem1  34691  satffunlem2lem1  34693  clsun  35516  lindsadd  36784  lindsenlbs  36786  poimirlem25  36816  poimirlem26  36817  poimirlem27  36818  cnambfre  36839  watvalN  39167  dnnumch1  42088  aomclem3  42100  aomclem8  42105  safesnsupfilb  42471  dssmapfv2d  43071  dssmapfv3d  43072  dssmapnvod  43073  clsk3nimkb  43093  ntrclscls00  43119  ntrclsiso  43120  ntrclsk3  43123  ntrclsk4  43125  nzprmdif  43380  compne  43502  dvmptfprodlem  44958  fouriercn  45246  meaiininclem  45500  meaiininc  45501  carageniuncllem1  45535  lindslinindsimp2  47231  ldepsnlinc  47276  line  47505  rrxline  47507  iscnrm3rlem4  47663