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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 3902

This theorem is used by:  difeq12d  4075  iinvdif  5040  otiunsndisj  5497  xpdifid  6160  imain  6618  dffv2  6973  f12dfv  7274  f13dfv  7275  tz7.49  8434  oev2  8510  difsnen  9057  domunsncan  9075  sbthlem2  9086  sbthlem3  9087  sbth  9095  rexdif1en  9155  dif1en  9156  sbthfi  9193  phplem2  9199  unblem2  9263  unblem3  9264  dfac8alem  10032  dfac8a  10033  kmlem9  10161  kmlem11  10163  kmlem12  10164  compsscnvlem  10372  s3iunsndisj  15041  isercolllem3  15754  ruclem13  16330  bitsf1  16536  setsvalg  17258  setsval  17259  setsdm  17262  ismri2dad  17725  mreexmrid  17731  mreexexlemd  17732  gsumvalx  18778  gsumpropd  18780  gsumpropd2lem  18781  gsumress  18784  pmtrfv  19579  gsumval3a  20030  gsumval3  20034  dprdcntz  20137  dprddisj  20138  dprdsn  20165  dprddisj2  20168  dpjval  20185  ablfac1eu  20202  drngprop  20907  subdrgint  20969  lbsind  21264  islbs2  21341  lbsextlem4  21348  lbsextg  21349  frlmlbs  22010  lindfind  22029  lindsind  22030  lindfrn  22034  f1lindf  22035  lindsenlbs  22064  submaval  22803  mdetunilem3  22836  mdetunilem4  22837  mdetunilem9  22842  clsval2  23275  ntrval2  23276  ntrdif  23277  clsdif  23278  cmclsopn  23287  islp  23365  pnrmopn  23568  hauscmplem  23631  bwth  23635  conndisj  23641  cvsunit  25359  bcthlem1  25552  bcth  25557  bcth3  25559  cmmbl  25762  nulmbl2  25764  shftmbl  25766  volsup  25784  mbfimaicc  25859  eldv  26125  ig1pval  26401  tglngval  28893  plngrotlem2  29145  lnssplng  29149  plng3p  29154  tgaaddcpbllem2  29229  axlowdimlem15  29413  axlowdim  29418  nbgr2vtx1edg  29810  nbuhgr2vtx1edgb  29812  nb3grprlem2  29841  uvtxel  29848  uvtxel1  29856  uvtxusgrel  29863  cusgredg  29884  cplgr1v  29890  cplgr3v  29895  usgredgsscusgredg  29919  usgr2pthlem  30228  2wspiundisj  30434  frcond1  30746  frgr1v  30751  nfrgr2v  30752  frgr3v  30755  1vwmgr  30756  3vfriswmgr  30758  3cyclfrgrrn1  30765  n4cyclfrgr  30771  frgrwopreglem4a  30790  supppreima  33163  odpmco  33526  tocycfv  33549  tocycf  33557  tocyc01  33558  cycpm2tr  33559  cycpmconjslem2  33595  cyc3conja  33597  0nellinds  33805  lindssn  33811  extvfval  34042  lbslsat  34126  lindsunlem  34134  ist0cld  34343  sigapildsyslem  34672  carsgclctunlem3  34831  sitgval  34843  ballotlemfval  35001  cplgredgex  35719  cvmscbv  35837  cvmsdisj  35849  cvmsss2  35853  satfv1  35942  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  clsun  36947  lindsadd  38367  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  cnambfre  38417  watvalN  40866  dnnumch1  43885  aomclem3  43897  aomclem8  43902  safesnsupfilb  44258  dssmapfv2d  44858  dssmapfv3d  44859  dssmapnvod  44860  clsk3nimkb  44880  ntrclscls00  44906  ntrclsiso  44907  ntrclsk3  44910  ntrclsk4  44912  nzprmdif  45143  compne  45264  dvmptfprodlem  46772  fouriercn  47060  meaiininclem  47314  meaiininc  47315  carageniuncllem1  47349  lindslinindsimp2  49393  ldepsnlinc  49438  line  49662  rrxline  49664  iscnrm3rlem4  49869