Theorem difeq2d 4089

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

Syntax hints:   → wi 4   = wceq 1567   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-dif 3916

This theorem is referenced by:  difeq12d  4090  iinvdif  5047  otiunsndisj  5501  xpdifid  6164  imain  6618  dffv2  6974  f12dfv  7269  f13dfv  7270  tz7.49  8428  oev2  8504  difsnen  9043  domunsncan  9061  sbthlem2  9072  sbthlem3  9073  sbth  9081  rexdif1en  9141  dif1en  9142  sbthfi  9179  phplem2  9185  unblem2  9249  unblem3  9250  dfac8alem  10009  dfac8a  10010  kmlem9  10138  kmlem11  10140  kmlem12  10141  compsscnvlem  10350  s3iunsndisj  15001  isercolllem3  15714  ruclem13  16294  bitsf1  16500  setsvalg  17222  setsval  17223  setsdm  17226  ismri2dad  17689  mreexmrid  17695  mreexexlemd  17696  gsumvalx  18730  gsumpropd  18732  gsumpropd2lem  18733  gsumress  18736  pmtrfv  19518  gsumval3a  19969  gsumval3  19973  dprdcntz  20076  dprddisj  20077  dprdsn  20104  dprddisj2  20107  dpjval  20124  ablfac1eu  20141  drngprop  20824  subdrgint  20880  lbsind  21175  islbs2  21252  lbsextlem4  21259  lbsextg  21260  frlmlbs  21912  lindfind  21931  lindsind  21932  lindfrn  21936  f1lindf  21937  submaval  22703  mdetunilem3  22736  mdetunilem4  22737  mdetunilem9  22742  clsval2  23172  ntrval2  23173  ntrdif  23174  clsdif  23175  cmclsopn  23184  islp  23262  pnrmopn  23465  hauscmplem  23528  bwth  23532  conndisj  23538  cvsunit  25255  bcthlem1  25448  bcth  25453  bcth3  25455  cmmbl  25658  nulmbl2  25660  shftmbl  25662  volsup  25680  mbfimaicc  25755  eldv  26022  ig1pval  26298  tglngval  28782  plngrotlem2  29024  lnssplng  29028  plng3p  29033  axlowdimlem15  29243  axlowdim  29248  nbgr2vtx1edg  29637  nbuhgr2vtx1edgb  29639  nb3grprlem2  29668  uvtxel  29675  uvtxel1  29683  uvtxusgrel  29690  cusgredg  29711  cplgr1v  29717  cplgr3v  29722  usgredgsscusgredg  29746  usgr2pthlem  30049  2wspiundisj  30252  frcond1  30554  frgr1v  30559  nfrgr2v  30560  frgr3v  30563  1vwmgr  30564  3vfriswmgr  30566  3cyclfrgrrn1  30573  n4cyclfrgr  30579  frgrwopreglem4a  30598  supppreima  32973  odpmco  33343  tocycfv  33366  tocycf  33374  tocyc01  33375  cycpm2tr  33376  cycpmconjslem2  33412  cyc3conja  33414  0nellinds  33624  lindssn  33631  extvfval  33863  lbslsat  33947  lindsunlem  33955  ist0cld  34164  sigapildsyslem  34492  carsgclctunlem3  34651  sitgval  34663  ballotlemfval  34821  cplgredgex  35508  cvmscbv  35645  cvmsdisj  35657  cvmsss2  35661  satfv1  35750  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  clsun  36724  lindsadd  38147  lindsenlbs  38149  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  cnambfre  38202  watvalN  40652  dnnumch1  43656  aomclem3  43668  aomclem8  43673  safesnsupfilb  44029  dssmapfv2d  44629  dssmapfv3d  44630  dssmapnvod  44631  clsk3nimkb  44651  ntrclscls00  44677  ntrclsiso  44678  ntrclsk3  44681  ntrclsk4  44683  nzprmdif  44914  compne  45035  dvmptfprodlem  46543  fouriercn  46831  meaiininclem  47085  meaiininc  47086  carageniuncllem1  47120  lindslinindsimp2  49121  ldepsnlinc  49166  line  49390  rrxline  49392  iscnrm3rlem4  49599