Theorem difeq1d 4083

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∖ cdif 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-dif 3911

This theorem is used by:  difeq12d  4085  dffv2  6983  on2recsov  8663  phplem2  9199  unfilem3  9277  marypha1lem  9403  infdifsn  9636  cantnfp1lem3  9659  en2other2  10012  isacn  10047  fin23lem28  10342  enfin1ai  10386  fin1a2lem7  10408  fzdifsuc  13631  axdc4uz  14040  leiso  14516  cshimadifsn  14892  isstruct2  17234  strle1  17243  setsfun0  17257  pltfval  18410  ischn  18688  chnind  18702  chnccats1  18706  chnccat  18707  f1omvdco2  19549  symgsssg  19568  symgfisg  19569  symggen  19571  pmtrdifellem3  19579  pmtrdifwrdellem3  19584  pmtrdifwrdel2lem1  19585  pmtrdifwrdel  19586  pmtrdifwrdel2  19587  psgnunilem1  19594  psgnunilem5  19595  psgnunilem2  19596  psgnunilem3  19597  gsumval3  20008  dmdprd  20101  dprd2da  20145  dmdprdsplit2lem  20148  dpjfval  20158  ablfac1eulem  20175  subdrgint  20943  lssset  21091  lbspropd  21257  islindf  21999  islindf2  22001  f1lindf  22009  opsrtoslem2  22244  cldval  23217  difopn  23228  mretopd  23286  restcld  23366  ordtcld1  23391  ordtcld2  23392  cnclima  23462  iscncl  23463  isreg2  23571  llycmpkgen2  23744  1stckgen  23748  ptval  23764  txcld  23797  ptcld  23807  txkgen  23846  qtopcld  23907  qtoprest  23911  qtopcmap  23913  kqcldsat  23927  regr1lem  23933  trufil  24104  ufildr  24125  opnsubg  24302  cldsubg  24305  blcld  24699  lebnumlem1  25157  bcthlem1  25520  bcth  25525  bcth3  25527  difmbl  25739  itg1val  25879  itgioo  26012  limciun  26090  dvfval  26093  newval  28065  noxpordpred  28183  istrkgl  28764  ishpg  29078  tgplnfn  29094  plngval  29096  isplng  29097  plng3p  29116  eengv  29366  elntg  29371  isuhgr  29447  isushgr  29448  uhgreq12g  29452  isuhgrop  29457  uhgr0vb  29459  uhgrun  29461  uhgrstrrepe  29465  isupgr  29471  upgrop  29481  isumgr  29482  upgrun  29505  isuspgr  29539  isusgr  29540  isuspgrop  29548  nb3grprlem2  29768  uvtxval  29774  nbupgruvtxres  29794  cplgrop  29824  cusgrexi  29830  structtocusgr  29833  1loopgrnb0  29889  cyclnumvtx  30186  isconngr1  30578  frgr3v  30663  difuncomp  32935  imadifxp  32983  fresunsn  33007  fressupp  33070  supppreima  33073  mptiffisupp  33075  gtiso  33083  difico  33165  fzdif2  33172  fzodif2  33173  fzodif1  33174  nn0diffz0  33176  pmtrcnel2  33441  cycpmconjvlem  33492  cycpmrn  33494  tocyccntz  33495  submarchi  33537  elrgspnlem4  33596  fracfld  33660  elrspunidl  33767  psrbasfsupp  33932  qtophaus  34257  difelsiga  34556  imambfm  34684  difelcarsg  34732  carsgclctunlem1  34739  carsggect  34740  issibf  34755  sibf0  34756  sitgfval  34763  ballotlemfval  34912  ballotlemfp1  34914  ballotlemgun  34947  hgt750lemb  35075  kur14  35729  iscvm  35772  cvmscld  35786  satf  35866  mdvval  36017  topbnd  36876  pibp21  38102  poimirlem2  38314  poimirlem4  38316  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem11  38323  poimirlem12  38324  poimirlem13  38325  poimirlem14  38326  poimirlem16  38328  poimirlem18  38330  poimirlem19  38331  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem27  38339  poimirlem30  38342  mblfinlem3  38351  mblfinlem4  38352  itg2addnclem  38363  itg2addnclem2  38364  prjspeclsp  43385  aomclem8  43829  kelac2  43833  gneispace2  44899  fzdifsuc2  46070  iccdifioo  46272  iccdifprioo  46273  ibliooicc  46726  dirkercncflem2  46859  issal  47069  prsal  47073  saldifcl2  47083  intsal  47085  sge0fodjrnlem  47171  caratheodorylem1  47281  vonvolmbllem  47415  salpreimagelt  47462  salpreimalegt  47464  smfresal  47543  chnsubseq  47637  dfnbgr5  48657  dfnbgr6  48663  isubgruhgr  48674  stgrnbgr0  48770  lines  49552  rrxlines  49554  eenglngeehlnm  49560  clddisj  49723  iscnrm3rlem1  49759