Theorem difeq1d 4012

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

Syntax hints:   → wi 4   = wceq 1542   ∖ cdif 3840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-dif 3846

This theorem is referenced by:  difeq12d  4014  dffv2  6763  phplem4  8749  unfilem3  8858  marypha1lem  8970  infdifsn  9193  cantnfp1lem3  9216  en2other2  9509  isacn  9544  fin23lem28  9840  enfin1ai  9884  fin1a2lem7  9906  fzdifsuc  13058  axdc4uz  13443  leiso  13911  cshimadifsn  14280  isstruct2  16596  setsfun0  16622  strle1  16695  pltfval  17685  f1omvdco2  18694  symgsssg  18713  symgfisg  18714  symggen  18716  pmtrdifellem3  18724  pmtrdifwrdellem3  18729  pmtrdifwrdel2lem1  18730  pmtrdifwrdel  18731  pmtrdifwrdel2  18732  psgnunilem1  18739  psgnunilem5  18740  psgnunilem2  18741  psgnunilem3  18742  gsumval3  19146  dmdprd  19239  dprd2da  19283  dmdprdsplit2lem  19286  dpjfval  19296  ablfac1eulem  19313  subdrgint  19701  lssset  19824  lbspropd  19990  islindf  20628  islindf2  20630  f1lindf  20638  opsrtoslem2  20867  cldval  21774  difopn  21785  mretopd  21843  restcld  21923  ordtcld1  21948  ordtcld2  21949  cnclima  22019  iscncl  22020  isreg2  22128  llycmpkgen2  22301  1stckgen  22305  ptval  22321  txcld  22354  ptcld  22364  txkgen  22403  qtopcld  22464  qtoprest  22468  qtopcmap  22470  kqcldsat  22484  regr1lem  22490  trufil  22661  ufildr  22682  opnsubg  22859  cldsubg  22862  blcld  23258  lebnumlem1  23713  bcthlem1  24076  bcth  24081  bcth3  24083  difmbl  24295  itg1val  24435  itgioo  24568  limciun  24646  dvfval  24649  istrkgl  26404  ishpg  26705  eengv  26925  elntg  26930  isuhgr  27005  isushgr  27006  uhgreq12g  27010  isuhgrop  27015  uhgr0vb  27017  uhgrun  27019  uhgrstrrepe  27023  isupgr  27029  upgrop  27039  isumgr  27040  upgrun  27063  isuspgr  27097  isusgr  27098  isuspgrop  27106  nb3grprlem2  27323  uvtxval  27329  nbupgruvtxres  27349  cplgrop  27379  cusgrexi  27385  structtocusgr  27388  1loopgrnb0  27444  isconngr1  28127  frgr3v  28212  difuncomp  30467  imadifxp  30514  fressupp  30597  supppreima  30600  gtiso  30608  difico  30679  fzdif2  30687  fzodif2  30688  fzodif1  30689  pmtrcnel2  30936  cycpmconjvlem  30985  cycpmrn  30987  tocyccntz  30988  submarchi  31017  elrspunidl  31178  qtophaus  31358  imambfm  31799  difelcarsg  31847  carsgclctunlem1  31854  carsggect  31855  issibf  31870  sibf0  31871  sitgfval  31878  ballotlemfval  32026  ballotlemfp1  32028  ballotlemgun  32061  hgt750lemb  32206  kur14  32749  iscvm  32792  cvmscld  32806  satf  32886  mdvval  33037  on2recsov  33470  newval  33682  noxpordpred  33753  topbnd  34156  pibp21  35229  poimirlem2  35422  poimirlem4  35424  poimirlem6  35426  poimirlem7  35427  poimirlem8  35428  poimirlem11  35431  poimirlem12  35432  poimirlem13  35433  poimirlem14  35434  poimirlem16  35436  poimirlem18  35438  poimirlem19  35439  poimirlem21  35441  poimirlem22  35442  poimirlem23  35443  poimirlem27  35447  poimirlem30  35450  mblfinlem3  35459  mblfinlem4  35460  itg2addnclem  35471  itg2addnclem2  35472  prjspeclsp  40048  aomclem8  40478  kelac2  40482  gneispace2  41308  fzdifsuc2  42407  iccdifioo  42613  iccdifprioo  42614  ibliooicc  43074  dirkercncflem2  43207  issal  43417  prsal  43421  saldifcl2  43429  intsal  43431  sge0fodjrnlem  43516  caratheodorylem1  43626  vonvolmbllem  43760  salpreimagelt  43804  salpreimalegt  43806  smfresal  43881  lines  45631  rrxlines  45633  eenglngeehlnm  45639  clddisj  45739  iscnrm3rlem1  45776