Theorem difeq2d 4068

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-dif 3900

This theorem is referenced by:  difeq12d  4069  iinvdif  5022  otiunsndisj  5453  xpdifid  6093  imain  6555  dffv2  6902  f12dfv  7184  f13dfv  7185  tz7.49  8323  oev2  8401  difsnen  8895  domunsncan  8914  sbthlem2  8926  sbthlem3  8927  sbth  8935  rexdif1en  9000  rexdif1enOLD  9001  dif1en  9002  dif1enOLD  9004  sbthfi  9044  phplem2  9050  phplem3OLD  9061  phplem4OLD  9062  unblem2  9137  unblem3  9138  xpfi  9155  dfac8alem  9858  dfac8a  9859  kmlem9  9987  kmlem11  9989  kmlem12  9990  compsscnvlem  10199  s3iunsndisj  14751  isercolllem3  15450  ruclem13  16023  bitsf1  16225  setsvalg  16937  setsval  16938  setsdm  16941  ismri2dad  17416  mreexmrid  17422  mreexexlemd  17423  gsumvalx  18430  gsumpropd  18432  gsumpropd2lem  18433  gsumress  18436  pmtrfv  19129  gsumval3a  19572  gsumval3  19576  dprdcntz  19679  dprddisj  19680  dprdsn  19707  dprddisj2  19710  dpjval  19727  ablfac1eu  19744  drngprop  20074  subdrgint  20143  lbsind  20414  islbs2  20488  lbsextlem4  20495  lbsextg  20496  frlmlbs  21076  lindfind  21095  lindsind  21096  lindfrn  21100  f1lindf  21101  submaval  21802  mdetunilem3  21835  mdetunilem4  21836  mdetunilem9  21841  clsval2  22273  ntrval2  22274  ntrdif  22275  clsdif  22276  cmclsopn  22285  islp  22363  pnrmopn  22566  hauscmplem  22629  bwth  22633  conndisj  22639  cvsunit  24366  bcthlem1  24560  bcth  24565  bcth3  24567  cmmbl  24770  nulmbl2  24772  shftmbl  24774  volsup  24792  mbfimaicc  24867  eldv  25134  ig1pval  25409  tglngval  27021  axlowdimlem15  27433  axlowdim  27438  nbgr2vtx1edg  27826  nbuhgr2vtx1edgb  27828  nb3grprlem2  27857  uvtxel  27864  uvtxel1  27872  uvtxusgrel  27879  cusgredg  27900  cplgr1v  27906  cplgr3v  27911  usgredgsscusgredg  27935  usgr2pthlem  28240  2wspiundisj  28437  frcond1  28739  frgr1v  28744  nfrgr2v  28745  frgr3v  28748  1vwmgr  28749  3vfriswmgr  28751  3cyclfrgrrn1  28758  n4cyclfrgr  28764  frgrwopreglem4a  28783  supppreima  31133  odpmco  31463  tocycfv  31484  tocycf  31492  tocyc01  31493  cycpm2tr  31494  cycpmconjslem2  31530  cyc3conja  31532  0nellinds  31671  lindssn  31678  lbslsat  31805  lindsunlem  31811  ist0cld  31889  sigapildsyslem  32235  carsgclctunlem3  32393  sitgval  32405  ballotlemfval  32562  cplgredgex  33187  cvmscbv  33325  cvmsdisj  33337  cvmsss2  33341  satfv1  33430  satffunlem  33468  satffunlem1lem1  33469  satffunlem2lem1  33471  clsun  34575  lindsadd  35826  lindsenlbs  35828  poimirlem25  35858  poimirlem26  35859  poimirlem27  35860  cnambfre  35881  watvalN  38212  dnnumch1  41073  aomclem3  41085  aomclem8  41090  dssmapfv2d  41847  dssmapfv3d  41848  dssmapnvod  41849  clsk3nimkb  41871  ntrclscls00  41897  ntrclsiso  41898  ntrclsk3  41901  ntrclsk4  41903  nzprmdif  42158  compne  42280  dvmptfprodlem  43722  fouriercn  44010  meaiininclem  44262  meaiininc  44263  carageniuncllem1  44297  lindslinindsimp2  46056  ldepsnlinc  46101  line  46330  rrxline  46332  iscnrm3rlem4  46489