Theorem difeq1d 4091

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920

This theorem is referenced by:  difeq12d  4093  dffv2  6959  on2recsov  8635  phplem2  9175  unfilem3  9263  marypha1lem  9391  infdifsn  9617  cantnfp1lem3  9640  en2other2  9969  isacn  10004  fin23lem28  10300  enfin1ai  10344  fin1a2lem7  10366  fzdifsuc  13552  axdc4uz  13956  leiso  14431  cshimadifsn  14802  isstruct2  17126  strle1  17135  setsfun0  17149  pltfval  18297  f1omvdco2  19385  symgsssg  19404  symgfisg  19405  symggen  19407  pmtrdifellem3  19415  pmtrdifwrdellem3  19420  pmtrdifwrdel2lem1  19421  pmtrdifwrdel  19422  pmtrdifwrdel2  19423  psgnunilem1  19430  psgnunilem5  19431  psgnunilem2  19432  psgnunilem3  19433  gsumval3  19844  dmdprd  19937  dprd2da  19981  dmdprdsplit2lem  19984  dpjfval  19994  ablfac1eulem  20011  subdrgint  20719  lssset  20846  lbspropd  21013  islindf  21728  islindf2  21730  f1lindf  21738  opsrtoslem2  21970  cldval  22917  difopn  22928  mretopd  22986  restcld  23066  ordtcld1  23091  ordtcld2  23092  cnclima  23162  iscncl  23163  isreg2  23271  llycmpkgen2  23444  1stckgen  23448  ptval  23464  txcld  23497  ptcld  23507  txkgen  23546  qtopcld  23607  qtoprest  23611  qtopcmap  23613  kqcldsat  23627  regr1lem  23633  trufil  23804  ufildr  23825  opnsubg  24002  cldsubg  24005  blcld  24400  lebnumlem1  24867  bcthlem1  25231  bcth  25236  bcth3  25238  difmbl  25451  itg1val  25591  itgioo  25724  limciun  25802  dvfval  25805  newval  27770  noxpordpred  27867  istrkgl  28392  ishpg  28693  eengv  28913  elntg  28918  isuhgr  28994  isushgr  28995  uhgreq12g  28999  isuhgrop  29004  uhgr0vb  29006  uhgrun  29008  uhgrstrrepe  29012  isupgr  29018  upgrop  29028  isumgr  29029  upgrun  29052  isuspgr  29086  isusgr  29087  isuspgrop  29095  nb3grprlem2  29315  uvtxval  29321  nbupgruvtxres  29341  cplgrop  29371  cusgrexi  29377  structtocusgr  29380  1loopgrnb0  29437  cyclnumvtx  29737  isconngr1  30126  frgr3v  30211  difuncomp  32489  imadifxp  32537  fressupp  32618  supppreima  32621  mptiffisupp  32623  gtiso  32631  difico  32713  fzdif2  32720  fzodif2  32721  fzodif1  32722  ischn  32939  chnind  32944  chnccats1  32948  pmtrcnel2  33054  cycpmconjvlem  33105  cycpmrn  33107  tocyccntz  33108  submarchi  33147  elrgspnlem4  33203  fracfld  33265  elrspunidl  33406  qtophaus  33833  imambfm  34260  difelcarsg  34308  carsgclctunlem1  34315  carsggect  34316  issibf  34331  sibf0  34332  sitgfval  34339  ballotlemfval  34488  ballotlemfp1  34490  ballotlemgun  34523  hgt750lemb  34654  kur14  35210  iscvm  35253  cvmscld  35267  satf  35347  mdvval  35498  topbnd  36319  pibp21  37410  poimirlem2  37623  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem16  37637  poimirlem18  37639  poimirlem19  37640  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem27  37648  poimirlem30  37651  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  itg2addnclem2  37673  prjspeclsp  42607  aomclem8  43057  kelac2  43061  gneispace2  44128  fzdifsuc2  45315  iccdifioo  45520  iccdifprioo  45521  ibliooicc  45976  dirkercncflem2  46109  issal  46319  prsal  46323  saldifcl2  46333  intsal  46335  sge0fodjrnlem  46421  caratheodorylem1  46531  vonvolmbllem  46665  salpreimagelt  46712  salpreimalegt  46714  smfresal  46793  dfnbgr5  47855  dfnbgr6  47861  isubgruhgr  47872  stgrnbgr0  47967  lines  48724  rrxlines  48726  eenglngeehlnm  48732  clddisj  48896  iscnrm3rlem1  48932