Theorem difeq2d 4120

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-dif 3950

This theorem is referenced by:  difeq12d  4121  iinvdif  5083  otiunsndisj  5522  xpdifid  6172  imain  6638  dffv2  6993  f12dfv  7282  f13dfv  7283  tz7.49  8466  oev2  8544  difsnen  9078  domunsncan  9097  sbthlem2  9109  sbthlem3  9110  sbth  9118  rexdif1en  9183  rexdif1enOLD  9184  dif1en  9185  dif1enOLD  9187  sbthfi  9227  phplem2  9233  phplem3OLD  9244  phplem4OLD  9245  unblem2  9321  unblem3  9322  xpfiOLD  9343  dfac8alem  10053  dfac8a  10054  kmlem9  10182  kmlem11  10184  kmlem12  10185  compsscnvlem  10394  s3iunsndisj  14948  isercolllem3  15646  ruclem13  16219  bitsf1  16421  setsvalg  17135  setsval  17136  setsdm  17139  ismri2dad  17617  mreexmrid  17623  mreexexlemd  17624  gsumvalx  18636  gsumpropd  18638  gsumpropd2lem  18639  gsumress  18642  pmtrfv  19407  gsumval3a  19858  gsumval3  19862  dprdcntz  19965  dprddisj  19966  dprdsn  19993  dprddisj2  19996  dpjval  20013  ablfac1eu  20030  drngprop  20639  subdrgint  20691  lbsind  20965  islbs2  21042  lbsextlem4  21049  lbsextg  21050  frlmlbs  21731  lindfind  21750  lindsind  21751  lindfrn  21755  f1lindf  21756  submaval  22496  mdetunilem3  22529  mdetunilem4  22530  mdetunilem9  22535  clsval2  22967  ntrval2  22968  ntrdif  22969  clsdif  22970  cmclsopn  22979  islp  23057  pnrmopn  23260  hauscmplem  23323  bwth  23327  conndisj  23333  cvsunit  25071  bcthlem1  25265  bcth  25270  bcth3  25272  cmmbl  25476  nulmbl2  25478  shftmbl  25480  volsup  25498  mbfimaicc  25573  eldv  25840  ig1pval  26123  tglngval  28368  axlowdimlem15  28780  axlowdim  28785  nbgr2vtx1edg  29176  nbuhgr2vtx1edgb  29178  nb3grprlem2  29207  uvtxel  29214  uvtxel1  29222  uvtxusgrel  29229  cusgredg  29250  cplgr1v  29256  cplgr3v  29261  usgredgsscusgredg  29286  usgr2pthlem  29590  2wspiundisj  29787  frcond1  30089  frgr1v  30094  nfrgr2v  30095  frgr3v  30098  1vwmgr  30099  3vfriswmgr  30101  3cyclfrgrrn1  30108  n4cyclfrgr  30114  frgrwopreglem4a  30133  supppreima  32484  odpmco  32822  tocycfv  32843  tocycf  32851  tocyc01  32852  cycpm2tr  32853  cycpmconjslem2  32889  cyc3conja  32891  0nellinds  33095  lindssn  33106  lbslsat  33314  lindsunlem  33322  ist0cld  33434  sigapildsyslem  33780  carsgclctunlem3  33940  sitgval  33952  ballotlemfval  34109  cplgredgex  34730  cvmscbv  34868  cvmsdisj  34880  cvmsss2  34884  satfv1  34973  satffunlem  35011  satffunlem1lem1  35012  satffunlem2lem1  35014  clsun  35812  lindsadd  37086  lindsenlbs  37088  poimirlem25  37118  poimirlem26  37119  poimirlem27  37120  cnambfre  37141  watvalN  39466  dnnumch1  42468  aomclem3  42480  aomclem8  42485  safesnsupfilb  42848  dssmapfv2d  43448  dssmapfv3d  43449  dssmapnvod  43450  clsk3nimkb  43470  ntrclscls00  43496  ntrclsiso  43497  ntrclsk3  43500  ntrclsk4  43502  nzprmdif  43756  compne  43878  dvmptfprodlem  45332  fouriercn  45620  meaiininclem  45874  meaiininc  45875  carageniuncllem1  45909  lindslinindsimp2  47531  ldepsnlinc  47576  line  47805  rrxline  47807  iscnrm3rlem4  47962