Theorem difeq2d 4126

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-dif 3954

This theorem is referenced by:  difeq12d  4127  iinvdif  5080  otiunsndisj  5525  xpdifid  6188  imain  6651  dffv2  7004  f12dfv  7293  f13dfv  7294  tz7.49  8485  oev2  8561  difsnen  9093  domunsncan  9112  sbthlem2  9124  sbthlem3  9125  sbth  9133  rexdif1en  9198  rexdif1enOLD  9199  dif1en  9200  dif1enOLD  9202  sbthfi  9239  phplem2  9245  phplem3OLD  9256  phplem4OLD  9257  unblem2  9329  unblem3  9330  xpfiOLD  9359  dfac8alem  10069  dfac8a  10070  kmlem9  10199  kmlem11  10201  kmlem12  10202  compsscnvlem  10410  s3iunsndisj  15007  isercolllem3  15703  ruclem13  16278  bitsf1  16483  setsvalg  17203  setsval  17204  setsdm  17207  ismri2dad  17680  mreexmrid  17686  mreexexlemd  17687  gsumvalx  18689  gsumpropd  18691  gsumpropd2lem  18692  gsumress  18695  pmtrfv  19470  gsumval3a  19921  gsumval3  19925  dprdcntz  20028  dprddisj  20029  dprdsn  20056  dprddisj2  20059  dpjval  20076  ablfac1eu  20093  drngprop  20744  subdrgint  20804  lbsind  21079  islbs2  21156  lbsextlem4  21163  lbsextg  21164  frlmlbs  21817  lindfind  21836  lindsind  21837  lindfrn  21841  f1lindf  21842  submaval  22587  mdetunilem3  22620  mdetunilem4  22621  mdetunilem9  22626  clsval2  23058  ntrval2  23059  ntrdif  23060  clsdif  23061  cmclsopn  23070  islp  23148  pnrmopn  23351  hauscmplem  23414  bwth  23418  conndisj  23424  cvsunit  25164  bcthlem1  25358  bcth  25363  bcth3  25365  cmmbl  25569  nulmbl2  25571  shftmbl  25573  volsup  25591  mbfimaicc  25666  eldv  25933  ig1pval  26215  tglngval  28559  axlowdimlem15  28971  axlowdim  28976  nbgr2vtx1edg  29367  nbuhgr2vtx1edgb  29369  nb3grprlem2  29398  uvtxel  29405  uvtxel1  29413  uvtxusgrel  29420  cusgredg  29441  cplgr1v  29447  cplgr3v  29452  usgredgsscusgredg  29477  usgr2pthlem  29783  2wspiundisj  29983  frcond1  30285  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  1vwmgr  30295  3vfriswmgr  30297  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrwopreglem4a  30329  supppreima  32700  odpmco  33106  tocycfv  33129  tocycf  33137  tocyc01  33138  cycpm2tr  33139  cycpmconjslem2  33175  cyc3conja  33177  0nellinds  33398  lindssn  33406  lbslsat  33667  lindsunlem  33675  ist0cld  33832  sigapildsyslem  34162  carsgclctunlem3  34322  sitgval  34334  ballotlemfval  34492  cplgredgex  35126  cvmscbv  35263  cvmsdisj  35275  cvmsss2  35279  satfv1  35368  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  clsun  36329  lindsadd  37620  lindsenlbs  37622  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  cnambfre  37675  watvalN  39995  dnnumch1  43056  aomclem3  43068  aomclem8  43073  safesnsupfilb  43431  dssmapfv2d  44031  dssmapfv3d  44032  dssmapnvod  44033  clsk3nimkb  44053  ntrclscls00  44079  ntrclsiso  44080  ntrclsk3  44083  ntrclsk4  44085  nzprmdif  44338  compne  44460  dvmptfprodlem  45959  fouriercn  46247  meaiininclem  46501  meaiininc  46502  carageniuncllem1  46536  lindslinindsimp2  48380  ldepsnlinc  48425  line  48653  rrxline  48655  iscnrm3rlem4  48840