Theorem difeq2d 4053

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  difeq12d  4054  iinvdif  5005  otiunsndisj  5428  xpdifid  6060  imain  6503  dffv2  6845  f12dfv  7126  f13dfv  7127  tz7.49  8246  oev2  8315  difsnen  8794  domunsncan  8812  sbthlem2  8824  sbthlem3  8825  sbth  8833  phplem3  8894  phplem4  8895  rexdif1en  8906  dif1en  8907  sbthfi  8942  unblem2  8997  unblem3  8998  xpfi  9015  dfac8alem  9716  dfac8a  9717  kmlem9  9845  kmlem11  9847  kmlem12  9848  compsscnvlem  10057  s3iunsndisj  14607  isercolllem3  15306  ruclem13  15879  bitsf1  16081  setsvalg  16795  setsval  16796  setsdm  16799  ismri2dad  17263  mreexmrid  17269  mreexexlemd  17270  gsumvalx  18275  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  pmtrfv  18975  gsumval3a  19419  gsumval3  19423  dprdcntz  19526  dprddisj  19527  dprdsn  19554  dprddisj2  19557  dpjval  19574  ablfac1eu  19591  drngprop  19917  subdrgint  19986  lbsind  20257  islbs2  20331  lbsextlem4  20338  lbsextg  20339  frlmlbs  20914  lindfind  20933  lindsind  20934  lindfrn  20938  f1lindf  20939  submaval  21638  mdetunilem3  21671  mdetunilem4  21672  mdetunilem9  21677  clsval2  22109  ntrval2  22110  ntrdif  22111  clsdif  22112  cmclsopn  22121  islp  22199  pnrmopn  22402  hauscmplem  22465  bwth  22469  conndisj  22475  cvsunit  24200  bcthlem1  24393  bcth  24398  bcth3  24400  cmmbl  24603  nulmbl2  24605  shftmbl  24607  volsup  24625  mbfimaicc  24700  eldv  24967  ig1pval  25242  tglngval  26816  axlowdimlem15  27227  axlowdim  27232  nbgr2vtx1edg  27620  nbuhgr2vtx1edgb  27622  nb3grprlem2  27651  uvtxel  27658  uvtxel1  27666  uvtxusgrel  27673  cusgredg  27694  cplgr1v  27700  cplgr3v  27705  usgredgsscusgredg  27729  usgr2pthlem  28032  2wspiundisj  28229  frcond1  28531  frgr1v  28536  nfrgr2v  28537  frgr3v  28540  1vwmgr  28541  3vfriswmgr  28543  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrwopreglem4a  28575  supppreima  30927  odpmco  31257  tocycfv  31278  tocycf  31286  tocyc01  31287  cycpm2tr  31288  cycpmconjslem2  31324  cyc3conja  31326  0nellinds  31468  lindssn  31475  lbslsat  31601  lindsunlem  31607  ist0cld  31685  sigapildsyslem  32029  carsgclctunlem3  32187  sitgval  32199  ballotlemfval  32356  cplgredgex  32982  cvmscbv  33120  cvmsdisj  33132  cvmsss2  33136  satfv1  33225  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  clsun  34444  lindsadd  35697  lindsenlbs  35699  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  cnambfre  35752  watvalN  37934  dnnumch1  40785  aomclem3  40797  aomclem8  40802  dssmapfv2d  41515  dssmapfv3d  41516  dssmapnvod  41517  clsk3nimkb  41539  ntrclscls00  41565  ntrclsiso  41566  ntrclsk3  41569  ntrclsk4  41571  nzprmdif  41826  compne  41948  dvmptfprodlem  43375  fouriercn  43663  meaiininclem  43914  meaiininc  43915  carageniuncllem1  43949  lindslinindsimp2  45692  ldepsnlinc  45737  line  45966  rrxline  45968  iscnrm3rlem4  46125