Theorem difeq1d 4066

Description: Deduction adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
difeq1d	⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Proof of Theorem difeq1d

Step	Hyp	Ref	Expression
1		difeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		difeq1 4060	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-dif 3893

This theorem is referenced by:  difeq12d  4068  dffv2  6929  on2recsov  8597  phplem2  9132  unfilem3  9210  marypha1lem  9339  infdifsn  9569  cantnfp1lem3  9592  en2other2  9922  isacn  9957  fin23lem28  10253  enfin1ai  10297  fin1a2lem7  10319  fzdifsuc  13529  axdc4uz  13937  leiso  14412  cshimadifsn  14782  isstruct2  17110  strle1  17119  setsfun0  17133  pltfval  18286  ischn  18564  chnind  18578  chnccats1  18582  chnccat  18583  f1omvdco2  19414  symgsssg  19433  symgfisg  19434  symggen  19436  pmtrdifellem3  19444  pmtrdifwrdellem3  19449  pmtrdifwrdel2lem1  19450  pmtrdifwrdel  19451  pmtrdifwrdel2  19452  psgnunilem1  19459  psgnunilem5  19460  psgnunilem2  19461  psgnunilem3  19462  gsumval3  19873  dmdprd  19966  dprd2da  20010  dmdprdsplit2lem  20013  dpjfval  20023  ablfac1eulem  20040  subdrgint  20771  lssset  20919  lbspropd  21086  islindf  21802  islindf2  21804  f1lindf  21812  opsrtoslem2  22044  cldval  22998  difopn  23009  mretopd  23067  restcld  23147  ordtcld1  23172  ordtcld2  23173  cnclima  23243  iscncl  23244  isreg2  23352  llycmpkgen2  23525  1stckgen  23529  ptval  23545  txcld  23578  ptcld  23588  txkgen  23627  qtopcld  23688  qtoprest  23692  qtopcmap  23694  kqcldsat  23708  regr1lem  23714  trufil  23885  ufildr  23906  opnsubg  24083  cldsubg  24086  blcld  24480  lebnumlem1  24938  bcthlem1  25301  bcth  25306  bcth3  25308  difmbl  25520  itg1val  25660  itgioo  25793  limciun  25871  dvfval  25874  newval  27841  noxpordpred  27959  istrkgl  28540  ishpg  28841  eengv  29062  elntg  29067  isuhgr  29143  isushgr  29144  uhgreq12g  29148  isuhgrop  29153  uhgr0vb  29155  uhgrun  29157  uhgrstrrepe  29161  isupgr  29167  upgrop  29177  isumgr  29178  upgrun  29201  isuspgr  29235  isusgr  29236  isuspgrop  29244  nb3grprlem2  29464  uvtxval  29470  nbupgruvtxres  29490  cplgrop  29520  cusgrexi  29526  structtocusgr  29529  1loopgrnb0  29586  cyclnumvtx  29883  isconngr1  30275  frgr3v  30360  difuncomp  32638  imadifxp  32686  fresunsn  32713  fressupp  32776  supppreima  32779  mptiffisupp  32781  gtiso  32789  difico  32871  fzdif2  32878  fzodif2  32879  fzodif1  32880  nn0diffz0  32882  pmtrcnel2  33166  cycpmconjvlem  33217  cycpmrn  33219  tocyccntz  33220  submarchi  33262  elrgspnlem4  33321  fracfld  33384  elrspunidl  33503  psrbasfsupp  33687  qtophaus  33996  imambfm  34422  difelcarsg  34470  carsgclctunlem1  34477  carsggect  34478  issibf  34493  sibf0  34494  sitgfval  34501  ballotlemfval  34650  ballotlemfp1  34652  ballotlemgun  34685  hgt750lemb  34816  kur14  35414  iscvm  35457  cvmscld  35471  satf  35551  mdvval  35702  topbnd  36522  pibp21  37745  poimirlem2  37957  poimirlem4  37959  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem14  37969  poimirlem16  37971  poimirlem18  37973  poimirlem19  37974  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem27  37982  poimirlem30  37985  mblfinlem3  37994  mblfinlem4  37995  itg2addnclem  38006  itg2addnclem2  38007  prjspeclsp  43059  aomclem8  43507  kelac2  43511  gneispace2  44577  fzdifsuc2  45761  iccdifioo  45963  iccdifprioo  45964  ibliooicc  46417  dirkercncflem2  46550  issal  46760  prsal  46764  saldifcl2  46774  intsal  46776  sge0fodjrnlem  46862  caratheodorylem1  46972  vonvolmbllem  47106  salpreimagelt  47153  salpreimalegt  47155  smfresal  47234  chnsubseq  47326  dfnbgr5  48339  dfnbgr6  48345  isubgruhgr  48356  stgrnbgr0  48452  lines  49219  rrxlines  49221  eenglngeehlnm  49227  clddisj  49391  iscnrm3rlem1  49427