Theorem difeq1d 4100

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-dif 3929

This theorem is referenced by:  difeq12d  4102  dffv2  6973  on2recsov  8678  phplem2  9217  unfilem3  9315  marypha1lem  9443  infdifsn  9669  cantnfp1lem3  9692  en2other2  10021  isacn  10056  fin23lem28  10352  enfin1ai  10396  fin1a2lem7  10418  fzdifsuc  13599  axdc4uz  14000  leiso  14475  cshimadifsn  14846  isstruct2  17166  strle1  17175  setsfun0  17189  pltfval  18339  f1omvdco2  19427  symgsssg  19446  symgfisg  19447  symggen  19449  pmtrdifellem3  19457  pmtrdifwrdellem3  19462  pmtrdifwrdel2lem1  19463  pmtrdifwrdel  19464  pmtrdifwrdel2  19465  psgnunilem1  19472  psgnunilem5  19473  psgnunilem2  19474  psgnunilem3  19475  gsumval3  19886  dmdprd  19979  dprd2da  20023  dmdprdsplit2lem  20026  dpjfval  20036  ablfac1eulem  20053  subdrgint  20761  lssset  20888  lbspropd  21055  islindf  21770  islindf2  21772  f1lindf  21780  opsrtoslem2  22012  cldval  22959  difopn  22970  mretopd  23028  restcld  23108  ordtcld1  23133  ordtcld2  23134  cnclima  23204  iscncl  23205  isreg2  23313  llycmpkgen2  23486  1stckgen  23490  ptval  23506  txcld  23539  ptcld  23549  txkgen  23588  qtopcld  23649  qtoprest  23653  qtopcmap  23655  kqcldsat  23669  regr1lem  23675  trufil  23846  ufildr  23867  opnsubg  24044  cldsubg  24047  blcld  24442  lebnumlem1  24909  bcthlem1  25274  bcth  25279  bcth3  25281  difmbl  25494  itg1val  25634  itgioo  25767  limciun  25845  dvfval  25848  newval  27811  noxpordpred  27903  istrkgl  28383  ishpg  28684  eengv  28904  elntg  28909  isuhgr  28985  isushgr  28986  uhgreq12g  28990  isuhgrop  28995  uhgr0vb  28997  uhgrun  28999  uhgrstrrepe  29003  isupgr  29009  upgrop  29019  isumgr  29020  upgrun  29043  isuspgr  29077  isusgr  29078  isuspgrop  29086  nb3grprlem2  29306  uvtxval  29312  nbupgruvtxres  29332  cplgrop  29362  cusgrexi  29368  structtocusgr  29371  1loopgrnb0  29428  cyclnumvtx  29728  isconngr1  30117  frgr3v  30202  difuncomp  32480  imadifxp  32528  fressupp  32611  supppreima  32614  mptiffisupp  32616  gtiso  32624  difico  32706  fzdif2  32713  fzodif2  32714  fzodif1  32715  ischn  32932  chnind  32937  chnccats1  32941  pmtrcnel2  33047  cycpmconjvlem  33098  cycpmrn  33100  tocyccntz  33101  submarchi  33130  elrgspnlem4  33186  fracfld  33248  elrspunidl  33389  qtophaus  33813  imambfm  34240  difelcarsg  34288  carsgclctunlem1  34295  carsggect  34296  issibf  34311  sibf0  34312  sitgfval  34319  ballotlemfval  34468  ballotlemfp1  34470  ballotlemgun  34503  hgt750lemb  34634  kur14  35184  iscvm  35227  cvmscld  35241  satf  35321  mdvval  35472  topbnd  36288  pibp21  37379  poimirlem2  37592  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem16  37606  poimirlem18  37608  poimirlem19  37609  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem27  37617  poimirlem30  37620  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  itg2addnclem2  37642  prjspeclsp  42582  aomclem8  43032  kelac2  43036  gneispace2  44103  fzdifsuc2  45287  iccdifioo  45492  iccdifprioo  45493  ibliooicc  45948  dirkercncflem2  46081  issal  46291  prsal  46295  saldifcl2  46305  intsal  46307  sge0fodjrnlem  46393  caratheodorylem1  46503  vonvolmbllem  46637  salpreimagelt  46684  salpreimalegt  46686  smfresal  46765  dfnbgr5  47812  dfnbgr6  47818  isubgruhgr  47829  stgrnbgr0  47924  lines  48659  rrxlines  48661  eenglngeehlnm  48667  clddisj  48826  iscnrm3rlem1  48862