Theorem difeq1d 4082

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

Syntax hints:   → wi 4   = wceq 1563   ∖ cdif 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-dif 3910

This theorem is referenced by:  difeq12d  4084  dffv2  6966  on2recsov  8642  phplem2  9177  unfilem3  9255  marypha1lem  9381  infdifsn  9614  cantnfp1lem3  9637  en2other2  9981  isacn  10016  fin23lem28  10312  enfin1ai  10356  fin1a2lem7  10378  fzdifsuc  13600  axdc4uz  14008  leiso  14484  cshimadifsn  14854  isstruct2  17197  strle1  17206  setsfun0  17220  pltfval  18373  ischn  18651  chnind  18665  chnccats1  18669  chnccat  18670  f1omvdco2  19506  symgsssg  19525  symgfisg  19526  symggen  19528  pmtrdifellem3  19536  pmtrdifwrdellem3  19541  pmtrdifwrdel2lem1  19542  pmtrdifwrdel  19543  pmtrdifwrdel2  19544  psgnunilem1  19551  psgnunilem5  19552  psgnunilem2  19553  psgnunilem3  19554  gsumval3  19965  dmdprd  20058  dprd2da  20102  dmdprdsplit2lem  20105  dpjfval  20115  ablfac1eulem  20132  subdrgint  20872  lssset  21020  lbspropd  21186  islindf  21919  islindf2  21921  f1lindf  21929  opsrtoslem2  22164  cldval  23137  difopn  23148  mretopd  23206  restcld  23286  ordtcld1  23311  ordtcld2  23312  cnclima  23382  iscncl  23383  isreg2  23491  llycmpkgen2  23664  1stckgen  23668  ptval  23684  txcld  23717  ptcld  23727  txkgen  23766  qtopcld  23827  qtoprest  23831  qtopcmap  23833  kqcldsat  23847  regr1lem  23853  trufil  24024  ufildr  24045  opnsubg  24222  cldsubg  24225  blcld  24619  lebnumlem1  25077  bcthlem1  25440  bcth  25445  bcth3  25447  difmbl  25659  itg1val  25799  itgioo  25932  limciun  26010  dvfval  26013  newval  27982  noxpordpred  28100  istrkgl  28681  ishpg  28986  tgplnfn  29001  plngval  29003  isplng  29004  plng3p  29019  eengv  29234  elntg  29239  isuhgr  29315  isushgr  29316  uhgreq12g  29320  isuhgrop  29325  uhgr0vb  29327  uhgrun  29329  uhgrstrrepe  29333  isupgr  29339  upgrop  29349  isumgr  29350  upgrun  29373  isuspgr  29407  isusgr  29408  isuspgrop  29416  nb3grprlem2  29636  uvtxval  29642  nbupgruvtxres  29662  cplgrop  29692  cusgrexi  29698  structtocusgr  29701  1loopgrnb0  29757  cyclnumvtx  30054  isconngr1  30446  frgr3v  30531  difuncomp  32804  imadifxp  32852  fresunsn  32878  fressupp  32941  supppreima  32944  mptiffisupp  32946  gtiso  32954  difico  33036  fzdif2  33043  fzodif2  33044  fzodif1  33045  nn0diffz0  33047  pmtrcnel2  33318  cycpmconjvlem  33369  cycpmrn  33371  tocyccntz  33372  submarchi  33414  elrgspnlem4  33473  fracfld  33539  elrspunidl  33647  psrbasfsupp  33813  qtophaus  34138  imambfm  34564  difelcarsg  34612  carsgclctunlem1  34619  carsggect  34620  issibf  34635  sibf0  34636  sitgfval  34643  ballotlemfval  34792  ballotlemfp1  34794  ballotlemgun  34827  hgt750lemb  34955  kur14  35574  iscvm  35617  cvmscld  35631  satf  35711  mdvval  35862  topbnd  36692  pibp21  37916  poimirlem2  38128  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem11  38137  poimirlem12  38138  poimirlem13  38139  poimirlem14  38140  poimirlem16  38142  poimirlem18  38144  poimirlem19  38145  poimirlem21  38147  poimirlem22  38148  poimirlem23  38149  poimirlem27  38153  poimirlem30  38156  mblfinlem3  38165  mblfinlem4  38166  itg2addnclem  38177  itg2addnclem2  38178  prjspeclsp  43201  aomclem8  43645  kelac2  43649  gneispace2  44715  fzdifsuc2  45888  iccdifioo  46090  iccdifprioo  46091  ibliooicc  46544  dirkercncflem2  46677  issal  46887  prsal  46891  saldifcl2  46901  intsal  46903  sge0fodjrnlem  46989  caratheodorylem1  47099  vonvolmbllem  47233  salpreimagelt  47280  salpreimalegt  47282  smfresal  47361  chnsubseq  47455  dfnbgr5  48472  dfnbgr6  48478  isubgruhgr  48489  stgrnbgr0  48585  lines  49363  rrxlines  49365  eenglngeehlnm  49371  clddisj  49534  iscnrm3rlem1  49570