Theorem difeq1d 4121

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

Syntax hints:   → wi 4   = wceq 1540   ∖ cdif 3945

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-dif 3951

This theorem is referenced by:  difeq12d  4123  dffv2  6986  on2recsov  8673  phplem2  9214  phplem4OLD  9226  unfilem3  9318  marypha1lem  9434  infdifsn  9658  cantnfp1lem3  9681  en2other2  10010  isacn  10045  fin23lem28  10341  enfin1ai  10385  fin1a2lem7  10407  fzdifsuc  13568  axdc4uz  13956  leiso  14427  cshimadifsn  14787  isstruct2  17089  strle1  17098  setsfun0  17112  pltfval  18294  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  20650  lssset  20776  lbspropd  20943  islindf  21677  islindf2  21679  f1lindf  21687  opsrtoslem2  21928  cldval  22847  difopn  22858  mretopd  22916  restcld  22996  ordtcld1  23021  ordtcld2  23022  cnclima  23092  iscncl  23093  isreg2  23201  llycmpkgen2  23374  1stckgen  23378  ptval  23394  txcld  23427  ptcld  23437  txkgen  23476  qtopcld  23537  qtoprest  23541  qtopcmap  23543  kqcldsat  23557  regr1lem  23563  trufil  23734  ufildr  23755  opnsubg  23932  cldsubg  23935  blcld  24334  lebnumlem1  24807  bcthlem1  25172  bcth  25177  bcth3  25179  difmbl  25392  itg1val  25532  itgioo  25665  limciun  25743  dvfval  25746  newval  27695  noxpordpred  27783  istrkgl  28142  ishpg  28443  eengv  28670  elntg  28675  isuhgr  28753  isushgr  28754  uhgreq12g  28758  isuhgrop  28763  uhgr0vb  28765  uhgrun  28767  uhgrstrrepe  28771  isupgr  28777  upgrop  28787  isumgr  28788  upgrun  28811  isuspgr  28845  isusgr  28846  isuspgrop  28854  nb3grprlem2  29071  uvtxval  29077  nbupgruvtxres  29097  cplgrop  29127  cusgrexi  29133  structtocusgr  29136  1loopgrnb0  29192  isconngr1  29876  frgr3v  29961  difuncomp  32218  imadifxp  32265  fressupp  32343  supppreima  32346  mptiffisupp  32348  gtiso  32355  difico  32427  fzdif2  32435  fzodif2  32436  fzodif1  32437  pmtrcnel2  32687  cycpmconjvlem  32736  cycpmrn  32738  tocyccntz  32739  submarchi  32768  elrspunidl  32986  qtophaus  33280  imambfm  33725  difelcarsg  33773  carsgclctunlem1  33780  carsggect  33781  issibf  33796  sibf0  33797  sitgfval  33804  ballotlemfval  33952  ballotlemfp1  33954  ballotlemgun  33987  hgt750lemb  34132  kur14  34671  iscvm  34714  cvmscld  34728  satf  34808  mdvval  34959  topbnd  35673  pibp21  36760  poimirlem2  36954  poimirlem4  36956  poimirlem6  36958  poimirlem7  36959  poimirlem8  36960  poimirlem11  36963  poimirlem12  36964  poimirlem13  36965  poimirlem14  36966  poimirlem16  36968  poimirlem18  36970  poimirlem19  36971  poimirlem21  36973  poimirlem22  36974  poimirlem23  36975  poimirlem27  36979  poimirlem30  36982  mblfinlem3  36991  mblfinlem4  36992  itg2addnclem  37003  itg2addnclem2  37004  prjspeclsp  41817  aomclem8  42266  kelac2  42270  gneispace2  43346  fzdifsuc2  44479  iccdifioo  44687  iccdifprioo  44688  ibliooicc  45146  dirkercncflem2  45279  issal  45489  prsal  45493  saldifcl2  45503  intsal  45505  sge0fodjrnlem  45591  caratheodorylem1  45701  vonvolmbllem  45835  salpreimagelt  45882  salpreimalegt  45884  smfresal  45963  lines  47579  rrxlines  47581  eenglngeehlnm  47587  clddisj  47698  iscnrm3rlem1  47735