Theorem difeq1d 4134

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

Syntax hints:   → wi 4   = wceq 1536   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-dif 3965

This theorem is referenced by:  difeq12d  4136  dffv2  7003  on2recsov  8704  phplem2  9242  phplem4OLD  9254  unfilem3  9342  marypha1lem  9470  infdifsn  9694  cantnfp1lem3  9717  en2other2  10046  isacn  10081  fin23lem28  10377  enfin1ai  10421  fin1a2lem7  10443  fzdifsuc  13620  axdc4uz  14021  leiso  14494  cshimadifsn  14864  isstruct2  17182  strle1  17191  setsfun0  17205  pltfval  18388  f1omvdco2  19480  symgsssg  19499  symgfisg  19500  symggen  19502  pmtrdifellem3  19510  pmtrdifwrdellem3  19515  pmtrdifwrdel2lem1  19516  pmtrdifwrdel  19517  pmtrdifwrdel2  19518  psgnunilem1  19525  psgnunilem5  19526  psgnunilem2  19527  psgnunilem3  19528  gsumval3  19939  dmdprd  20032  dprd2da  20076  dmdprdsplit2lem  20079  dpjfval  20089  ablfac1eulem  20106  subdrgint  20820  lssset  20948  lbspropd  21115  islindf  21849  islindf2  21851  f1lindf  21859  opsrtoslem2  22097  cldval  23046  difopn  23057  mretopd  23115  restcld  23195  ordtcld1  23220  ordtcld2  23221  cnclima  23291  iscncl  23292  isreg2  23400  llycmpkgen2  23573  1stckgen  23577  ptval  23593  txcld  23626  ptcld  23636  txkgen  23675  qtopcld  23736  qtoprest  23740  qtopcmap  23742  kqcldsat  23756  regr1lem  23762  trufil  23933  ufildr  23954  opnsubg  24131  cldsubg  24134  blcld  24533  lebnumlem1  25006  bcthlem1  25371  bcth  25376  bcth3  25378  difmbl  25591  itg1val  25731  itgioo  25865  limciun  25943  dvfval  25946  newval  27908  noxpordpred  28000  istrkgl  28480  ishpg  28781  eengv  29008  elntg  29013  isuhgr  29091  isushgr  29092  uhgreq12g  29096  isuhgrop  29101  uhgr0vb  29103  uhgrun  29105  uhgrstrrepe  29109  isupgr  29115  upgrop  29125  isumgr  29126  upgrun  29149  isuspgr  29183  isusgr  29184  isuspgrop  29192  nb3grprlem2  29412  uvtxval  29418  nbupgruvtxres  29438  cplgrop  29468  cusgrexi  29474  structtocusgr  29477  1loopgrnb0  29534  isconngr1  30218  frgr3v  30303  difuncomp  32573  imadifxp  32620  fressupp  32702  supppreima  32705  mptiffisupp  32707  gtiso  32715  difico  32791  fzdif2  32798  fzodif2  32799  fzodif1  32800  ischn  32980  chnind  32984  pmtrcnel2  33092  cycpmconjvlem  33143  cycpmrn  33145  tocyccntz  33146  submarchi  33175  elrgspnlem4  33234  fracfld  33289  elrspunidl  33435  qtophaus  33796  imambfm  34243  difelcarsg  34291  carsgclctunlem1  34298  carsggect  34299  issibf  34314  sibf0  34315  sitgfval  34322  ballotlemfval  34470  ballotlemfp1  34472  ballotlemgun  34505  hgt750lemb  34649  kur14  35200  iscvm  35243  cvmscld  35257  satf  35337  mdvval  35488  topbnd  36306  pibp21  37397  poimirlem2  37608  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem16  37622  poimirlem18  37624  poimirlem19  37625  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem27  37633  poimirlem30  37636  mblfinlem3  37645  mblfinlem4  37646  itg2addnclem  37657  itg2addnclem2  37658  prjspeclsp  42598  aomclem8  43049  kelac2  43053  gneispace2  44121  fzdifsuc2  45260  iccdifioo  45467  iccdifprioo  45468  ibliooicc  45926  dirkercncflem2  46059  issal  46269  prsal  46273  saldifcl2  46283  intsal  46285  sge0fodjrnlem  46371  caratheodorylem1  46481  vonvolmbllem  46615  salpreimagelt  46662  salpreimalegt  46664  smfresal  46743  dfnbgr5  47774  dfnbgr6  47780  isubgruhgr  47791  stgrnbgr0  47866  lines  48580  rrxlines  48582  eenglngeehlnm  48588  clddisj  48699  iscnrm3rlem1  48736