Theorem difeq1d 4074

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

Syntax hints:   → wi 4   = wceq 1541   ∖ cdif 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-dif 3901

This theorem is referenced by:  difeq12d  4076  dffv2  6925  on2recsov  8591  phplem2  9123  unfilem3  9200  marypha1lem  9326  infdifsn  9556  cantnfp1lem3  9579  en2other2  9909  isacn  9944  fin23lem28  10240  enfin1ai  10284  fin1a2lem7  10306  fzdifsuc  13488  axdc4uz  13895  leiso  14370  cshimadifsn  14740  isstruct2  17064  strle1  17073  setsfun0  17087  pltfval  18239  ischn  18517  chnind  18531  chnccats1  18535  chnccat  18536  f1omvdco2  19364  symgsssg  19383  symgfisg  19384  symggen  19386  pmtrdifellem3  19394  pmtrdifwrdellem3  19399  pmtrdifwrdel2lem1  19400  pmtrdifwrdel  19401  pmtrdifwrdel2  19402  psgnunilem1  19409  psgnunilem5  19410  psgnunilem2  19411  psgnunilem3  19412  gsumval3  19823  dmdprd  19916  dprd2da  19960  dmdprdsplit2lem  19963  dpjfval  19973  ablfac1eulem  19990  subdrgint  20722  lssset  20870  lbspropd  21037  islindf  21753  islindf2  21755  f1lindf  21763  opsrtoslem2  21994  cldval  22941  difopn  22952  mretopd  23010  restcld  23090  ordtcld1  23115  ordtcld2  23116  cnclima  23186  iscncl  23187  isreg2  23295  llycmpkgen2  23468  1stckgen  23472  ptval  23488  txcld  23521  ptcld  23531  txkgen  23570  qtopcld  23631  qtoprest  23635  qtopcmap  23637  kqcldsat  23651  regr1lem  23657  trufil  23828  ufildr  23849  opnsubg  24026  cldsubg  24029  blcld  24423  lebnumlem1  24890  bcthlem1  25254  bcth  25259  bcth3  25261  difmbl  25474  itg1val  25614  itgioo  25747  limciun  25825  dvfval  25828  newval  27799  noxpordpred  27899  istrkgl  28439  ishpg  28740  eengv  28961  elntg  28966  isuhgr  29042  isushgr  29043  uhgreq12g  29047  isuhgrop  29052  uhgr0vb  29054  uhgrun  29056  uhgrstrrepe  29060  isupgr  29066  upgrop  29076  isumgr  29077  upgrun  29100  isuspgr  29134  isusgr  29135  isuspgrop  29143  nb3grprlem2  29363  uvtxval  29369  nbupgruvtxres  29389  cplgrop  29419  cusgrexi  29425  structtocusgr  29428  1loopgrnb0  29485  cyclnumvtx  29782  isconngr1  30174  frgr3v  30259  difuncomp  32537  imadifxp  32585  fressupp  32675  supppreima  32678  mptiffisupp  32680  gtiso  32688  difico  32772  fzdif2  32779  fzodif2  32780  fzodif1  32781  nn0diffz0  32783  pmtrcnel2  33068  cycpmconjvlem  33119  cycpmrn  33121  tocyccntz  33122  submarchi  33164  elrgspnlem4  33221  fracfld  33283  elrspunidl  33402  psrbasfsupp  33581  qtophaus  33872  imambfm  34298  difelcarsg  34346  carsgclctunlem1  34353  carsggect  34354  issibf  34369  sibf0  34370  sitgfval  34377  ballotlemfval  34526  ballotlemfp1  34528  ballotlemgun  34561  hgt750lemb  34692  kur14  35283  iscvm  35326  cvmscld  35340  satf  35420  mdvval  35571  topbnd  36391  pibp21  37482  poimirlem2  37685  poimirlem4  37687  poimirlem6  37689  poimirlem7  37690  poimirlem8  37691  poimirlem11  37694  poimirlem12  37695  poimirlem13  37696  poimirlem14  37697  poimirlem16  37699  poimirlem18  37701  poimirlem19  37702  poimirlem21  37704  poimirlem22  37705  poimirlem23  37706  poimirlem27  37710  poimirlem30  37713  mblfinlem3  37722  mblfinlem4  37723  itg2addnclem  37734  itg2addnclem2  37735  prjspeclsp  42733  aomclem8  43181  kelac2  43185  gneispace2  44252  fzdifsuc2  45438  iccdifioo  45642  iccdifprioo  45643  ibliooicc  46096  dirkercncflem2  46229  issal  46439  prsal  46443  saldifcl2  46453  intsal  46455  sge0fodjrnlem  46541  caratheodorylem1  46651  vonvolmbllem  46785  salpreimagelt  46832  salpreimalegt  46834  smfresal  46913  chnsubseq  47005  dfnbgr5  47978  dfnbgr6  47984  isubgruhgr  47995  stgrnbgr0  48091  lines  48859  rrxlines  48861  eenglngeehlnm  48867  clddisj  49031  iscnrm3rlem1  49067