Theorem difeq2d 4081

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-dif 3909

This theorem is used by:  difeq12d  4082  iinvdif  5048  otiunsndisj  5505  xpdifid  6167  imain  6625  dffv2  6980  f12dfv  7277  f13dfv  7278  tz7.49  8434  oev2  8510  difsnen  9050  domunsncan  9068  sbthlem2  9079  sbthlem3  9080  sbth  9088  rexdif1en  9148  dif1en  9149  sbthfi  9186  phplem2  9192  unblem2  9256  unblem3  9257  dfac8alem  10025  dfac8a  10026  kmlem9  10154  kmlem11  10156  kmlem12  10157  compsscnvlem  10365  s3iunsndisj  15024  isercolllem3  15737  ruclem13  16315  bitsf1  16521  setsvalg  17243  setsval  17244  setsdm  17247  ismri2dad  17710  mreexmrid  17716  mreexexlemd  17717  gsumvalx  18755  gsumpropd  18757  gsumpropd2lem  18758  gsumress  18761  pmtrfv  19545  gsumval3a  19996  gsumval3  20000  dprdcntz  20103  dprddisj  20104  dprdsn  20131  dprddisj2  20134  dpjval  20151  ablfac1eu  20168  drngprop  20873  subdrgint  20935  lbsind  21230  islbs2  21307  lbsextlem4  21314  lbsextg  21315  frlmlbs  21976  lindfind  21995  lindsind  21996  lindfrn  22000  f1lindf  22001  submaval  22767  mdetunilem3  22800  mdetunilem4  22801  mdetunilem9  22806  clsval2  23236  ntrval2  23237  ntrdif  23238  clsdif  23239  cmclsopn  23248  islp  23326  pnrmopn  23529  hauscmplem  23592  bwth  23596  conndisj  23602  cvsunit  25319  bcthlem1  25512  bcth  25517  bcth3  25519  cmmbl  25722  nulmbl2  25724  shftmbl  25726  volsup  25744  mbfimaicc  25819  eldv  26086  ig1pval  26362  tglngval  28849  plngrotlem2  29099  lnssplng  29103  plng3p  29108  axlowdimlem15  29335  axlowdim  29340  nbgr2vtx1edg  29729  nbuhgr2vtx1edgb  29731  nb3grprlem2  29760  uvtxel  29767  uvtxel1  29775  uvtxusgrel  29782  cusgredg  29803  cplgr1v  29809  cplgr3v  29814  usgredgsscusgredg  29838  usgr2pthlem  30141  2wspiundisj  30344  frcond1  30646  frgr1v  30651  nfrgr2v  30652  frgr3v  30655  1vwmgr  30656  3vfriswmgr  30658  3cyclfrgrrn1  30665  n4cyclfrgr  30671  frgrwopreglem4a  30690  supppreima  33065  odpmco  33429  tocycfv  33452  tocycf  33460  tocyc01  33461  cycpm2tr  33462  cycpmconjslem2  33498  cyc3conja  33500  0nellinds  33708  lindssn  33714  extvfval  33945  lbslsat  34029  lindsunlem  34037  ist0cld  34246  sigapildsyslem  34575  carsgclctunlem3  34734  sitgval  34746  ballotlemfval  34904  cplgredgex  35626  cvmscbv  35763  cvmsdisj  35775  cvmsss2  35779  satfv1  35868  satffunlem  35906  satffunlem1lem1  35907  satffunlem2lem1  35909  clsun  36872  lindsadd  38297  lindsenlbs  38299  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  cnambfre  38352  watvalN  40800  dnnumch1  43804  aomclem3  43816  aomclem8  43821  safesnsupfilb  44177  dssmapfv2d  44777  dssmapfv3d  44778  dssmapnvod  44779  clsk3nimkb  44799  ntrclscls00  44825  ntrclsiso  44826  ntrclsk3  44829  ntrclsk4  44831  nzprmdif  45062  compne  45183  dvmptfprodlem  46691  fouriercn  46979  meaiininclem  47233  meaiininc  47234  carageniuncllem1  47268  lindslinindsimp2  49276  ldepsnlinc  49321  line  49545  rrxline  49547  iscnrm3rlem4  49754