Theorem difeq2d 4101

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3923

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-dif 3929

This theorem is referenced by:  difeq12d  4102  iinvdif  5056  otiunsndisj  5495  xpdifid  6157  imain  6620  dffv2  6973  f12dfv  7265  f13dfv  7266  tz7.49  8457  oev2  8533  difsnen  9065  domunsncan  9084  sbthlem2  9096  sbthlem3  9097  sbth  9105  rexdif1en  9170  rexdif1enOLD  9171  dif1en  9172  dif1enOLD  9174  sbthfi  9211  phplem2  9217  phplem3OLD  9228  unblem2  9299  unblem3  9300  xpfiOLD  9329  dfac8alem  10041  dfac8a  10042  kmlem9  10171  kmlem11  10173  kmlem12  10174  compsscnvlem  10382  s3iunsndisj  14985  isercolllem3  15681  ruclem13  16258  bitsf1  16463  setsvalg  17183  setsval  17184  setsdm  17187  ismri2dad  17647  mreexmrid  17653  mreexexlemd  17654  gsumvalx  18652  gsumpropd  18654  gsumpropd2lem  18655  gsumress  18658  pmtrfv  19431  gsumval3a  19882  gsumval3  19886  dprdcntz  19989  dprddisj  19990  dprdsn  20017  dprddisj2  20020  dpjval  20037  ablfac1eu  20054  drngprop  20702  subdrgint  20761  lbsind  21036  islbs2  21113  lbsextlem4  21120  lbsextg  21121  frlmlbs  21755  lindfind  21774  lindsind  21775  lindfrn  21779  f1lindf  21780  submaval  22517  mdetunilem3  22550  mdetunilem4  22551  mdetunilem9  22556  clsval2  22986  ntrval2  22987  ntrdif  22988  clsdif  22989  cmclsopn  22998  islp  23076  pnrmopn  23279  hauscmplem  23342  bwth  23346  conndisj  23352  cvsunit  25080  bcthlem1  25274  bcth  25279  bcth3  25281  cmmbl  25485  nulmbl2  25487  shftmbl  25489  volsup  25507  mbfimaicc  25582  eldv  25849  ig1pval  26131  tglngval  28476  axlowdimlem15  28881  axlowdim  28886  nbgr2vtx1edg  29275  nbuhgr2vtx1edgb  29277  nb3grprlem2  29306  uvtxel  29313  uvtxel1  29321  uvtxusgrel  29328  cusgredg  29349  cplgr1v  29355  cplgr3v  29360  usgredgsscusgredg  29385  usgr2pthlem  29691  2wspiundisj  29891  frcond1  30193  frgr1v  30198  nfrgr2v  30199  frgr3v  30202  1vwmgr  30203  3vfriswmgr  30205  3cyclfrgrrn1  30212  n4cyclfrgr  30218  frgrwopreglem4a  30237  supppreima  32614  odpmco  33043  tocycfv  33066  tocycf  33074  tocyc01  33075  cycpm2tr  33076  cycpmconjslem2  33112  cyc3conja  33114  0nellinds  33331  lindssn  33339  lbslsat  33602  lindsunlem  33610  ist0cld  33810  sigapildsyslem  34138  carsgclctunlem3  34298  sitgval  34310  ballotlemfval  34468  cplgredgex  35089  cvmscbv  35226  cvmsdisj  35238  cvmsss2  35242  satfv1  35331  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  clsun  36292  lindsadd  37583  lindsenlbs  37585  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  cnambfre  37638  watvalN  39958  dnnumch1  43015  aomclem3  43027  aomclem8  43032  safesnsupfilb  43389  dssmapfv2d  43989  dssmapfv3d  43990  dssmapnvod  43991  clsk3nimkb  44011  ntrclscls00  44037  ntrclsiso  44038  ntrclsk3  44041  ntrclsk4  44043  nzprmdif  44291  compne  44413  dvmptfprodlem  45921  fouriercn  46209  meaiininclem  46463  meaiininc  46464  carageniuncllem1  46498  lindslinindsimp2  48387  ldepsnlinc  48432  line  48660  rrxline  48662  iscnrm3rlem4  48865