Theorem difeq1d 4077

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904

This theorem is referenced by:  difeq12d  4079  dffv2  6929  on2recsov  8596  phplem2  9129  unfilem3  9207  marypha1lem  9336  infdifsn  9566  cantnfp1lem3  9589  en2other2  9919  isacn  9954  fin23lem28  10250  enfin1ai  10294  fin1a2lem7  10316  fzdifsuc  13500  axdc4uz  13907  leiso  14382  cshimadifsn  14752  isstruct2  17076  strle1  17085  setsfun0  17099  pltfval  18252  ischn  18530  chnind  18544  chnccats1  18548  chnccat  18549  f1omvdco2  19377  symgsssg  19396  symgfisg  19397  symggen  19399  pmtrdifellem3  19407  pmtrdifwrdellem3  19412  pmtrdifwrdel2lem1  19413  pmtrdifwrdel  19414  pmtrdifwrdel2  19415  psgnunilem1  19422  psgnunilem5  19423  psgnunilem2  19424  psgnunilem3  19425  gsumval3  19836  dmdprd  19929  dprd2da  19973  dmdprdsplit2lem  19976  dpjfval  19986  ablfac1eulem  20003  subdrgint  20736  lssset  20884  lbspropd  21051  islindf  21767  islindf2  21769  f1lindf  21777  opsrtoslem2  22011  cldval  22967  difopn  22978  mretopd  23036  restcld  23116  ordtcld1  23141  ordtcld2  23142  cnclima  23212  iscncl  23213  isreg2  23321  llycmpkgen2  23494  1stckgen  23498  ptval  23514  txcld  23547  ptcld  23557  txkgen  23596  qtopcld  23657  qtoprest  23661  qtopcmap  23663  kqcldsat  23677  regr1lem  23683  trufil  23854  ufildr  23875  opnsubg  24052  cldsubg  24055  blcld  24449  lebnumlem1  24916  bcthlem1  25280  bcth  25285  bcth3  25287  difmbl  25500  itg1val  25640  itgioo  25773  limciun  25851  dvfval  25854  newval  27831  noxpordpred  27949  istrkgl  28530  ishpg  28831  eengv  29052  elntg  29057  isuhgr  29133  isushgr  29134  uhgreq12g  29138  isuhgrop  29143  uhgr0vb  29145  uhgrun  29147  uhgrstrrepe  29151  isupgr  29157  upgrop  29167  isumgr  29168  upgrun  29191  isuspgr  29225  isusgr  29226  isuspgrop  29234  nb3grprlem2  29454  uvtxval  29460  nbupgruvtxres  29480  cplgrop  29510  cusgrexi  29516  structtocusgr  29519  1loopgrnb0  29576  cyclnumvtx  29873  isconngr1  30265  frgr3v  30350  difuncomp  32628  imadifxp  32676  fresunsn  32703  fressupp  32767  supppreima  32770  mptiffisupp  32772  gtiso  32780  difico  32863  fzdif2  32870  fzodif2  32871  fzodif1  32872  nn0diffz0  32874  pmtrcnel2  33172  cycpmconjvlem  33223  cycpmrn  33225  tocyccntz  33226  submarchi  33268  elrgspnlem4  33327  fracfld  33390  elrspunidl  33509  psrbasfsupp  33693  qtophaus  33993  imambfm  34419  difelcarsg  34467  carsgclctunlem1  34474  carsggect  34475  issibf  34490  sibf0  34491  sitgfval  34498  ballotlemfval  34647  ballotlemfp1  34649  ballotlemgun  34682  hgt750lemb  34813  kur14  35410  iscvm  35453  cvmscld  35467  satf  35547  mdvval  35698  topbnd  36518  pibp21  37620  poimirlem2  37823  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem18  37839  poimirlem19  37840  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem27  37848  poimirlem30  37851  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem  37872  itg2addnclem2  37873  prjspeclsp  42855  aomclem8  43303  kelac2  43307  gneispace2  44373  fzdifsuc2  45558  iccdifioo  45761  iccdifprioo  45762  ibliooicc  46215  dirkercncflem2  46348  issal  46558  prsal  46562  saldifcl2  46572  intsal  46574  sge0fodjrnlem  46660  caratheodorylem1  46770  vonvolmbllem  46904  salpreimagelt  46951  salpreimalegt  46953  smfresal  47032  chnsubseq  47124  dfnbgr5  48097  dfnbgr6  48103  isubgruhgr  48114  stgrnbgr0  48210  lines  48977  rrxlines  48979  eenglngeehlnm  48985  clddisj  49149  iscnrm3rlem1  49185