Theorem difeq2d 4074

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12d  4075  iinvdif  5040  otiunsndisj  5493  xpdifid  6159  imain  6623  dffv2  6978  f12dfv  7279  f13dfv  7280  tz7.49  8448  oev2  8524  difsnen  9071  domunsncan  9089  sbthlem2  9100  sbthlem3  9101  sbth  9109  rexdif1en  9169  dif1en  9170  sbthfi  9207  phplem2  9213  unblem2  9278  unblem3  9279  dfac8alem  10101  dfac8a  10102  kmlem9  10230  kmlem11  10232  kmlem12  10233  compsscnvlem  10441  s3iunsndisj  15114  isercolllem3  15827  ruclem13  16403  bitsf1  16609  setsvalg  17337  setsval  17338  setsdm  17341  ismri2dad  17804  mreexmrid  17810  mreexexlemd  17811  gsumvalx  18858  gsumpropd  18860  gsumpropd2lem  18861  gsumress  18864  pmtrfv  19659  gsumval3a  20110  gsumval3  20114  dprdcntz  20217  dprddisj  20218  dprdsn  20245  dprddisj2  20248  dpjval  20265  ablfac1eu  20282  drngprop  20991  subdrgint  21053  lbsind  21348  islbs2  21425  lbsextlem4  21432  lbsextg  21433  frlmlbs  22096  lindfind  22115  lindsind  22116  lindfrn  22120  f1lindf  22121  lindsenlbs  22150  submaval  22889  mdetunilem3  22922  mdetunilem4  22923  mdetunilem9  22928  clsval2  23361  ntrval2  23362  ntrdif  23363  clsdif  23364  cmclsopn  23373  islp  23451  pnrmopn  23654  hauscmplem  23717  bwth  23721  conndisj  23727  cvsunit  25445  bcthlem1  25638  bcth  25643  bcth3  25645  cmmbl  25848  nulmbl2  25850  shftmbl  25852  volsup  25870  mbfimaicc  25945  eldv  26211  ig1pval  26487  tglngval  29007  plngrotlem2  29259  lnssplng  29263  plng3p  29268  tgaaddcpbllem2  29343  axlowdimlem15  29527  axlowdim  29532  nbgr2vtx1edg  29924  nbuhgr2vtx1edgb  29926  nb3grprlem2  29955  uvtxel  29962  uvtxel1  29970  uvtxusgrel  29977  cusgredg  29998  cplgr1v  30004  cplgr3v  30009  usgredgsscusgredg  30033  usgr2pthlem  30342  2wspiundisj  30548  frcond1  30860  frgr1v  30865  nfrgr2v  30866  frgr3v  30869  1vwmgr  30870  3vfriswmgr  30872  3cyclfrgrrn1  30879  n4cyclfrgr  30885  frgrwopreglem4a  30904  supppreima  33277  odpmco  33640  tocycfv  33663  tocycf  33671  tocyc01  33672  cycpm2tr  33673  cycpmconjslem2  33709  cyc3conja  33711  0nellinds  33919  lindssn  33926  extvfval  34157  lbslsat  34241  lindsunlem  34249  ist0cld  34458  sigapildsyslem  34787  carsgclctunlem3  34945  sitgval  34957  ballotlemfval  35115  cplgredgex  35884  cvmscbv  36002  cvmsdisj  36014  cvmsss2  36018  satfv1  36107  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  clsun  37096  lindsadd  38516  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  cnambfre  38566  watvalN  41030  dnnumch1  44030  aomclem3  44042  aomclem8  44047  safesnsupfilb  44403  dssmapfv2d  45003  dssmapfv3d  45004  dssmapnvod  45005  clsk3nimkb  45025  ntrclscls00  45051  ntrclsiso  45052  ntrclsk3  45055  ntrclsk4  45057  nzprmdif  45288  compne  45409  dvmptfprodlem  46923  fouriercn  47211  meaiininclem  47465  meaiininc  47466  carageniuncllem1  47500  lindslinindsimp2  49544  ldepsnlinc  49589  line  49813  rrxline  49815  iscnrm3rlem4  50020