Theorem difeq2d 4082

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

Syntax hints:   → wi 4   = wceq 1570   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-dif 3909

This theorem is referenced by:  difeq12d  4083  iinvdif  5047  otiunsndisj  5505  xpdifid  6167  imain  6623  dffv2  6978  f12dfv  7273  f13dfv  7274  tz7.49  8433  oev2  8509  difsnen  9048  domunsncan  9066  sbthlem2  9077  sbthlem3  9078  sbth  9086  rexdif1en  9146  dif1en  9147  sbthfi  9184  phplem2  9190  unblem2  9254  unblem3  9255  dfac8alem  10014  dfac8a  10015  kmlem9  10143  kmlem11  10145  kmlem12  10146  compsscnvlem  10355  s3iunsndisj  15007  isercolllem3  15720  ruclem13  16299  bitsf1  16505  setsvalg  17227  setsval  17228  setsdm  17231  ismri2dad  17694  mreexmrid  17700  mreexexlemd  17701  gsumvalx  18735  gsumpropd  18737  gsumpropd2lem  18738  gsumress  18741  pmtrfv  19523  gsumval3a  19974  gsumval3  19978  dprdcntz  20081  dprddisj  20082  dprdsn  20109  dprddisj2  20112  dpjval  20129  ablfac1eu  20146  drngprop  20831  subdrgint  20887  lbsind  21182  islbs2  21259  lbsextlem4  21266  lbsextg  21267  frlmlbs  21928  lindfind  21947  lindsind  21948  lindfrn  21952  f1lindf  21953  submaval  22719  mdetunilem3  22752  mdetunilem4  22753  mdetunilem9  22758  clsval2  23188  ntrval2  23189  ntrdif  23190  clsdif  23191  cmclsopn  23200  islp  23278  pnrmopn  23481  hauscmplem  23544  bwth  23548  conndisj  23554  cvsunit  25271  bcthlem1  25464  bcth  25469  bcth3  25471  cmmbl  25674  nulmbl2  25676  shftmbl  25678  volsup  25696  mbfimaicc  25771  eldv  26038  ig1pval  26314  tglngval  28801  plngrotlem2  29051  lnssplng  29055  plng3p  29060  axlowdimlem15  29287  axlowdim  29292  nbgr2vtx1edg  29681  nbuhgr2vtx1edgb  29683  nb3grprlem2  29712  uvtxel  29719  uvtxel1  29727  uvtxusgrel  29734  cusgredg  29755  cplgr1v  29761  cplgr3v  29766  usgredgsscusgredg  29790  usgr2pthlem  30093  2wspiundisj  30296  frcond1  30598  frgr1v  30603  nfrgr2v  30604  frgr3v  30607  1vwmgr  30608  3vfriswmgr  30610  3cyclfrgrrn1  30617  n4cyclfrgr  30623  frgrwopreglem4a  30642  supppreima  33017  odpmco  33387  tocycfv  33410  tocycf  33418  tocyc01  33419  cycpm2tr  33420  cycpmconjslem2  33456  cyc3conja  33458  0nellinds  33666  lindssn  33672  extvfval  33903  lbslsat  33987  lindsunlem  33995  ist0cld  34204  sigapildsyslem  34532  carsgclctunlem3  34691  sitgval  34703  ballotlemfval  34861  cplgredgex  35594  cvmscbv  35731  cvmsdisj  35743  cvmsss2  35747  satfv1  35836  satffunlem  35874  satffunlem1lem1  35875  satffunlem2lem1  35877  clsun  36820  lindsadd  38245  lindsenlbs  38247  poimirlem25  38277  poimirlem26  38278  poimirlem27  38279  cnambfre  38300  watvalN  40748  dnnumch1  43754  aomclem3  43766  aomclem8  43771  safesnsupfilb  44127  dssmapfv2d  44727  dssmapfv3d  44728  dssmapnvod  44729  clsk3nimkb  44749  ntrclscls00  44775  ntrclsiso  44776  ntrclsk3  44779  ntrclsk4  44781  nzprmdif  45012  compne  45133  dvmptfprodlem  46641  fouriercn  46929  meaiininclem  47183  meaiininc  47184  carageniuncllem1  47218  lindslinindsimp2  49226  ldepsnlinc  49271  line  49495  rrxline  49497  iscnrm3rlem4  49704