Theorem difeq2d 4066

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  difeq12d  4067  iinvdif  5045  otiunsndisj  5500  xpdifid  6177  imain  6655  dffv2  7011  f12dfv  7312  f13dfv  7313  tz7.49  8493  oev2  8569  difsnen  9116  domunsncan  9134  sbthlem2  9145  sbthlem3  9146  sbth  9154  rexdif1en  9214  dif1en  9215  sbthfi  9252  phplem2  9258  unblem2  9323  unblem3  9324  dfac8alem  10147  dfac8a  10148  kmlem9  10276  kmlem11  10278  kmlem12  10279  compsscnvlem  10487  s3iunsndisj  15164  isercolllem3  15878  ruclem13  16454  bitsf1  16660  setsvalg  17388  setsval  17389  setsdm  17392  ismri2dad  17861  mreexmrid  17867  mreexexlemd  17868  gsumvalx  18915  gsumpropd  18917  gsumpropd2lem  18918  gsumress  18921  pmtrfv  19717  gsumval3a  20168  gsumval3  20172  dprdcntz  20275  dprddisj  20276  dprdsn  20303  dprddisj2  20306  dpjval  20323  ablfac1eu  20340  drngprop  21049  subdrgint  21111  lbsind  21406  islbs2  21483  lbsextlem4  21490  lbsextg  21491  frlmlbs  22158  lindfind  22177  lindsind  22178  lindfrn  22182  f1lindf  22183  lindsenlbs  22212  submaval  22951  mdetunilem3  22984  mdetunilem4  22985  mdetunilem9  22990  clsval2  23423  ntrval2  23424  ntrdif  23425  clsdif  23426  cmclsopn  23435  islp  23513  pnrmopn  23716  hauscmplem  23779  bwth  23783  conndisj  23789  cvsunit  25507  bcthlem1  25700  bcth  25705  bcth3  25707  cmmbl  25910  nulmbl2  25912  shftmbl  25914  volsup  25932  mbfimaicc  26007  eldv  26273  ig1pval  26549  tglngval  29071  plngrotlem2  29323  lnssplng  29327  plng3p  29332  tgaaddcpbllem2  29407  axlowdimlem15  29591  axlowdim  29596  nbgr2vtx1edg  29988  nbuhgr2vtx1edgb  29990  nb3grprlem2  30019  uvtxel  30026  uvtxel1  30034  uvtxusgrel  30041  cusgredg  30062  cplgr1v  30068  cplgr3v  30073  usgredgsscusgredg  30097  usgr2pthlem  30406  2wspiundisj  30612  frcond1  30924  frgr1v  30929  nfrgr2v  30930  frgr3v  30933  1vwmgr  30934  3vfriswmgr  30936  3cyclfrgrrn1  30943  n4cyclfrgr  30949  frgrwopreglem4a  30968  supppreima  33381  odpmco  33746  tocycfv  33769  tocycf  33777  tocyc01  33778  cycpm2tr  33779  cycpmconjslem2  33815  cyc3conja  33817  isedom  33953  0nellinds  34030  lindssn  34037  extvfval  34275  lbslsat  34359  lindsunlem  34367  ist0cld  34576  sigapildsyslem  34905  carsgclctunlem3  35063  sitgval  35075  ballotlemfval  35233  cplgredgex  36103  cvmscbv  36231  cvmsdisj  36243  cvmsss2  36247  satfv1  36336  satffunlem  36374  satffunlem1lem1  36375  satffunlem2lem1  36377  clsun  37331  lindsadd  38804  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  cnambfre  38854  watvalN  41316  dnnumch1  44317  aomclem3  44324  aomclem8  44329  safesnsupfilb  44680  dssmapfv2d  45279  dssmapfv3d  45280  dssmapnvod  45281  clsk3nimkb  45301  ntrclscls00  45327  ntrclsiso  45328  ntrclsk3  45331  ntrclsk4  45333  nzprmdif  45564  compne  45684  dvmptfprodlem  47227  fouriercn  47515  meaiininclem  47769  meaiininc  47770  carageniuncllem1  47804  lindslinindsimp2  49906  ldepsnlinc  49951  line  50176  rrxline  50178  iscnrm3rlem4  50388