Theorem difeq2d 4099

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

Syntax hints:   → wi 4   = wceq 1533   ∖ cdif 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-dif 3939

This theorem is referenced by:  difeq12d  4100  iinvdif  4995  otiunsndisj  5403  xpdifid  6020  imain  6434  dffv2  6751  f12dfv  7024  f13dfv  7025  tz7.49  8075  oev2  8142  difsnen  8593  domunsncan  8611  sbthlem2  8622  sbthlem3  8623  sbth  8631  phplem3  8692  phplem4  8693  unblem2  8765  unblem3  8766  xpfi  8783  dfac8alem  9449  dfac8a  9450  kmlem9  9578  kmlem11  9580  kmlem12  9581  compsscnvlem  9786  s3iunsndisj  14322  isercolllem3  15017  ruclem13  15589  bitsf1  15789  setsvalg  16506  setsval  16507  setsdm  16511  ismri2dad  16902  mreexmrid  16908  mreexexlemd  16909  gsumvalx  17880  gsumpropd  17882  gsumpropd2lem  17883  gsumress  17886  pmtrfv  18574  gsumval3a  19017  gsumval3  19021  dprdcntz  19124  dprddisj  19125  dprdsn  19152  dprddisj2  19155  dpjval  19172  ablfac1eu  19189  drngprop  19507  subdrgint  19576  lbsind  19846  islbs2  19920  lbsextlem4  19927  lbsextg  19928  frlmlbs  20935  lindfind  20954  lindsind  20955  lindfrn  20959  f1lindf  20960  submaval  21184  mdetunilem3  21217  mdetunilem4  21218  mdetunilem9  21223  clsval2  21652  ntrval2  21653  ntrdif  21654  clsdif  21655  cmclsopn  21664  islp  21742  pnrmopn  21945  hauscmplem  22008  bwth  22012  conndisj  22018  cvsunit  23729  bcthlem1  23921  bcth  23926  bcth3  23928  cmmbl  24129  nulmbl2  24131  shftmbl  24133  volsup  24151  mbfimaicc  24226  eldv  24490  ig1pval  24760  tglngval  26331  axlowdimlem15  26736  axlowdim  26741  nbgr2vtx1edg  27126  nbuhgr2vtx1edgb  27128  nb3grprlem2  27157  uvtxel  27164  uvtxel1  27172  uvtxusgrel  27179  cusgredg  27200  cplgr1v  27206  cplgr3v  27211  usgredgsscusgredg  27235  usgr2pthlem  27538  2wspiundisj  27736  frcond1  28039  frgr1v  28044  nfrgr2v  28045  frgr3v  28048  1vwmgr  28049  3vfriswmgr  28051  3cyclfrgrrn1  28058  n4cyclfrgr  28064  frgrwopreglem4a  28083  odpmco  30725  tocycfv  30746  tocycf  30754  tocyc01  30755  cycpm2tr  30756  cycpmconjslem2  30792  cyc3conja  30794  0nellinds  30930  lindssn  30934  lbslsat  31009  lindsunlem  31015  sigapildsyslem  31415  carsgclctunlem3  31573  sitgval  31585  ballotlemfval  31742  cplgredgex  32362  cvmscbv  32500  cvmsdisj  32512  cvmsss2  32516  satfv1  32605  satffunlem  32643  satffunlem1lem1  32644  satffunlem2lem1  32646  clsun  33671  lindsadd  34879  lindsenlbs  34881  poimirlem25  34911  poimirlem26  34912  poimirlem27  34913  cnambfre  34934  watvalN  37123  dnnumch1  39637  aomclem3  39649  aomclem8  39654  dssmapfv2d  40357  dssmapfv3d  40358  dssmapnvod  40359  clsk3nimkb  40383  ntrclscls00  40409  ntrclsiso  40410  ntrclsk3  40413  ntrclsk4  40415  nzprmdif  40644  compne  40766  dvmptfprodlem  42221  fouriercn  42510  meaiininclem  42761  meaiininc  42762  carageniuncllem1  42796  lindslinindsimp2  44511  ldepsnlinc  44556  line  44712  rrxline  44714