Theorem difeq1d 4086

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-dif 3916

This theorem is referenced by:  difeq12d  4088  dffv2  6941  on2recsov  8619  phplem2  9159  phplem4OLD  9171  unfilem3  9263  marypha1lem  9378  infdifsn  9602  cantnfp1lem3  9625  en2other2  9954  isacn  9989  fin23lem28  10285  enfin1ai  10329  fin1a2lem7  10351  fzdifsuc  13511  axdc4uz  13899  leiso  14370  cshimadifsn  14730  isstruct2  17032  strle1  17041  setsfun0  17055  pltfval  18234  f1omvdco2  19244  symgsssg  19263  symgfisg  19264  symggen  19266  pmtrdifellem3  19274  pmtrdifwrdellem3  19279  pmtrdifwrdel2lem1  19280  pmtrdifwrdel  19281  pmtrdifwrdel2  19282  psgnunilem1  19289  psgnunilem5  19290  psgnunilem2  19291  psgnunilem3  19292  gsumval3  19698  dmdprd  19791  dprd2da  19835  dmdprdsplit2lem  19838  dpjfval  19848  ablfac1eulem  19865  subdrgint  20326  lssset  20451  lbspropd  20617  islindf  21255  islindf2  21257  f1lindf  21265  opsrtoslem2  21500  cldval  22411  difopn  22422  mretopd  22480  restcld  22560  ordtcld1  22585  ordtcld2  22586  cnclima  22656  iscncl  22657  isreg2  22765  llycmpkgen2  22938  1stckgen  22942  ptval  22958  txcld  22991  ptcld  23001  txkgen  23040  qtopcld  23101  qtoprest  23105  qtopcmap  23107  kqcldsat  23121  regr1lem  23127  trufil  23298  ufildr  23319  opnsubg  23496  cldsubg  23499  blcld  23898  lebnumlem1  24361  bcthlem1  24725  bcth  24730  bcth3  24732  difmbl  24944  itg1val  25084  itgioo  25217  limciun  25295  dvfval  25298  newval  27228  noxpordpred  27308  istrkgl  27463  ishpg  27764  eengv  27991  elntg  27996  isuhgr  28074  isushgr  28075  uhgreq12g  28079  isuhgrop  28084  uhgr0vb  28086  uhgrun  28088  uhgrstrrepe  28092  isupgr  28098  upgrop  28108  isumgr  28109  upgrun  28132  isuspgr  28166  isusgr  28167  isuspgrop  28175  nb3grprlem2  28392  uvtxval  28398  nbupgruvtxres  28418  cplgrop  28448  cusgrexi  28454  structtocusgr  28457  1loopgrnb0  28513  isconngr1  29197  frgr3v  29282  difuncomp  31539  imadifxp  31586  fressupp  31670  supppreima  31673  mptiffisupp  31675  gtiso  31682  difico  31754  fzdif2  31762  fzodif2  31763  fzodif1  31764  pmtrcnel2  32011  cycpmconjvlem  32060  cycpmrn  32062  tocyccntz  32063  submarchi  32092  elrspunidl  32279  qtophaus  32506  imambfm  32951  difelcarsg  32999  carsgclctunlem1  33006  carsggect  33007  issibf  33022  sibf0  33023  sitgfval  33030  ballotlemfval  33178  ballotlemfp1  33180  ballotlemgun  33213  hgt750lemb  33358  kur14  33897  iscvm  33940  cvmscld  33954  satf  34034  mdvval  34185  topbnd  34872  pibp21  35959  poimirlem2  36153  poimirlem4  36155  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem11  36162  poimirlem12  36163  poimirlem13  36164  poimirlem14  36165  poimirlem16  36167  poimirlem18  36169  poimirlem19  36170  poimirlem21  36172  poimirlem22  36173  poimirlem23  36174  poimirlem27  36178  poimirlem30  36181  mblfinlem3  36190  mblfinlem4  36191  itg2addnclem  36202  itg2addnclem2  36203  prjspeclsp  41008  aomclem8  41446  kelac2  41450  gneispace2  42526  fzdifsuc2  43665  iccdifioo  43873  iccdifprioo  43874  ibliooicc  44332  dirkercncflem2  44465  issal  44675  prsal  44679  saldifcl2  44689  intsal  44691  sge0fodjrnlem  44777  caratheodorylem1  44887  vonvolmbllem  45021  salpreimagelt  45068  salpreimalegt  45070  smfresal  45149  lines  46937  rrxlines  46939  eenglngeehlnm  46945  clddisj  47056  iscnrm3rlem1  47093