Theorem difeq2d 3991

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

Syntax hints:   → wi 4   = wceq 1508   ∖ cdif 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-ral 3095  df-rab 3099  df-dif 3834

This theorem is referenced by:  difeq12d  3992  iinvdif  4873  otiunsndisj  5270  xpdifid  5870  imain  6277  dffv2  6590  f12dfv  6861  f13dfv  6862  tz7.49  7890  oev2  7956  difsnen  8401  domunsncan  8419  sbthlem2  8430  sbthlem3  8431  sbth  8439  phplem3  8500  phplem4  8501  unblem2  8572  unblem3  8573  xpfi  8590  dfac8alem  9255  dfac8a  9256  kmlem9  9384  kmlem11  9386  kmlem12  9387  compsscnvlem  9596  s3iunsndisj  14195  isercolllem3  14890  ruclem13  15461  bitsf1  15661  setsvalg  16374  setsval  16375  setsdm  16379  ismri2dad  16778  mreexmrid  16784  mreexexlemd  16785  gsumvalx  17750  gsumpropd  17752  gsumpropd2lem  17753  gsumress  17756  pmtrfv  18353  gsumval3a  18789  gsumval3  18793  dprdcntz  18892  dprddisj  18893  dprdsn  18920  dprddisj2  18923  dpjval  18940  ablfac1eu  18957  drngprop  19248  subdrgint  19316  lbsind  19586  islbs2  19660  lbsextlem4  19667  lbsextg  19668  frlmlbs  20658  lindfind  20677  lindsind  20678  lindfrn  20682  f1lindf  20683  submaval  20909  mdetunilem3  20942  mdetunilem4  20943  mdetunilem9  20948  clsval2  21377  ntrval2  21378  ntrdif  21379  clsdif  21380  cmclsopn  21389  islp  21467  pnrmopn  21670  hauscmplem  21733  bwth  21737  conndisj  21743  cvsunit  23453  bcthlem1  23645  bcth  23650  bcth3  23652  cmmbl  23853  nulmbl2  23855  shftmbl  23857  volsup  23875  mbfimaicc  23950  eldv  24214  ig1pval  24484  tglngval  26054  axlowdimlem15  26460  axlowdim  26465  nbgr2vtx1edg  26850  nbuhgr2vtx1edgb  26852  nb3grprlem2  26881  uvtxel  26888  uvtxel1  26896  uvtxusgrel  26903  cusgredg  26924  cplgr1v  26930  cplgr3v  26935  usgredgsscusgredg  26959  usgr2pthlem  27267  2wspiundisj  27484  frcond1  27815  frgr1v  27820  nfrgr2v  27821  frgr3v  27824  1vwmgr  27825  3vfriswmgr  27827  3cyclfrgrrn1  27834  n4cyclfrgr  27840  frgrwopreglem4a  27859  tocycfv  30473  tocycf  30479  cycpm2tr  30480  0nellinds  30640  lindssn  30642  lbslsat  30675  lindsunlem  30681  sigapildsyslem  31097  carsgclctunlem3  31255  sitgval  31267  ballotlemfval  31425  cvmscbv  32130  cvmsdisj  32142  cvmsss2  32146  clsun  33237  lindsadd  34366  lindsenlbs  34368  poimirlem25  34398  poimirlem26  34399  poimirlem27  34400  cnambfre  34421  watvalN  36614  dnnumch1  39081  aomclem3  39093  aomclem8  39098  dssmapfv2d  39768  dssmapfv3d  39769  dssmapnvod  39770  clsk3nimkb  39794  ntrclscls00  39820  ntrclsiso  39821  ntrclsk3  39824  ntrclsk4  39826  nzprmdif  40108  compne  40232  dvmptfprodlem  41694  fouriercn  41983  meaiininclem  42234  meaiininc  42235  carageniuncllem1  42269  lindslinindsimp2  43920  ldepsnlinc  43965  line  44122  rrxline  44124