Theorem difeq1d 4052

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886

This theorem is referenced by:  difeq12d  4054  dffv2  6845  phplem4  8895  unfilem3  9010  marypha1lem  9122  infdifsn  9345  cantnfp1lem3  9368  en2other2  9696  isacn  9731  fin23lem28  10027  enfin1ai  10071  fin1a2lem7  10093  fzdifsuc  13245  axdc4uz  13632  leiso  14101  cshimadifsn  14470  isstruct2  16778  strle1  16787  setsfun0  16801  pltfval  17964  f1omvdco2  18971  symgsssg  18990  symgfisg  18991  symggen  18993  pmtrdifellem3  19001  pmtrdifwrdellem3  19006  pmtrdifwrdel2lem1  19007  pmtrdifwrdel  19008  pmtrdifwrdel2  19009  psgnunilem1  19016  psgnunilem5  19017  psgnunilem2  19018  psgnunilem3  19019  gsumval3  19423  dmdprd  19516  dprd2da  19560  dmdprdsplit2lem  19563  dpjfval  19573  ablfac1eulem  19590  subdrgint  19986  lssset  20110  lbspropd  20276  islindf  20929  islindf2  20931  f1lindf  20939  opsrtoslem2  21173  cldval  22082  difopn  22093  mretopd  22151  restcld  22231  ordtcld1  22256  ordtcld2  22257  cnclima  22327  iscncl  22328  isreg2  22436  llycmpkgen2  22609  1stckgen  22613  ptval  22629  txcld  22662  ptcld  22672  txkgen  22711  qtopcld  22772  qtoprest  22776  qtopcmap  22778  kqcldsat  22792  regr1lem  22798  trufil  22969  ufildr  22990  opnsubg  23167  cldsubg  23170  blcld  23567  lebnumlem1  24030  bcthlem1  24393  bcth  24398  bcth3  24400  difmbl  24612  itg1val  24752  itgioo  24885  limciun  24963  dvfval  24966  istrkgl  26723  ishpg  27024  eengv  27250  elntg  27255  isuhgr  27333  isushgr  27334  uhgreq12g  27338  isuhgrop  27343  uhgr0vb  27345  uhgrun  27347  uhgrstrrepe  27351  isupgr  27357  upgrop  27367  isumgr  27368  upgrun  27391  isuspgr  27425  isusgr  27426  isuspgrop  27434  nb3grprlem2  27651  uvtxval  27657  nbupgruvtxres  27677  cplgrop  27707  cusgrexi  27713  structtocusgr  27716  1loopgrnb0  27772  isconngr1  28455  frgr3v  28540  difuncomp  30794  imadifxp  30841  fressupp  30924  supppreima  30927  gtiso  30935  difico  31006  fzdif2  31014  fzodif2  31015  fzodif1  31016  pmtrcnel2  31261  cycpmconjvlem  31310  cycpmrn  31312  tocyccntz  31313  submarchi  31342  elrspunidl  31508  qtophaus  31688  imambfm  32129  difelcarsg  32177  carsgclctunlem1  32184  carsggect  32185  issibf  32200  sibf0  32201  sitgfval  32208  ballotlemfval  32356  ballotlemfp1  32358  ballotlemgun  32391  hgt750lemb  32536  kur14  33078  iscvm  33121  cvmscld  33135  satf  33215  mdvval  33366  on2recsov  33754  newval  33966  noxpordpred  34037  topbnd  34440  pibp21  35513  poimirlem2  35706  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem16  35720  poimirlem18  35722  poimirlem19  35723  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem27  35731  poimirlem30  35734  mblfinlem3  35743  mblfinlem4  35744  itg2addnclem  35755  itg2addnclem2  35756  prjspeclsp  40372  aomclem8  40802  kelac2  40806  gneispace2  41631  fzdifsuc2  42739  iccdifioo  42943  iccdifprioo  42944  ibliooicc  43402  dirkercncflem2  43535  issal  43745  prsal  43749  saldifcl2  43757  intsal  43759  sge0fodjrnlem  43844  caratheodorylem1  43954  vonvolmbllem  44088  salpreimagelt  44132  salpreimalegt  44134  smfresal  44209  lines  45965  rrxlines  45967  eenglngeehlnm  45973  clddisj  46085  iscnrm3rlem1  46122