Theorem difeq1d 4081

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

Syntax hints:   → wi 4   = wceq 1570   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-dif 3909

This theorem is referenced by:  difeq12d  4083  dffv2  6978  on2recsov  8655  phplem2  9190  unfilem3  9268  marypha1lem  9394  infdifsn  9627  cantnfp1lem3  9650  en2other2  9994  isacn  10029  fin23lem28  10325  enfin1ai  10369  fin1a2lem7  10391  fzdifsuc  13614  axdc4uz  14022  leiso  14498  cshimadifsn  14868  isstruct2  17210  strle1  17219  setsfun0  17233  pltfval  18386  ischn  18664  chnind  18678  chnccats1  18682  chnccat  18683  f1omvdco2  19519  symgsssg  19538  symgfisg  19539  symggen  19541  pmtrdifellem3  19549  pmtrdifwrdellem3  19554  pmtrdifwrdel2lem1  19555  pmtrdifwrdel  19556  pmtrdifwrdel2  19557  psgnunilem1  19564  psgnunilem5  19565  psgnunilem2  19566  psgnunilem3  19567  gsumval3  19978  dmdprd  20071  dprd2da  20115  dmdprdsplit2lem  20118  dpjfval  20128  ablfac1eulem  20145  subdrgint  20887  lssset  21035  lbspropd  21201  islindf  21943  islindf2  21945  f1lindf  21953  opsrtoslem2  22188  cldval  23161  difopn  23172  mretopd  23230  restcld  23310  ordtcld1  23335  ordtcld2  23336  cnclima  23406  iscncl  23407  isreg2  23515  llycmpkgen2  23688  1stckgen  23692  ptval  23708  txcld  23741  ptcld  23751  txkgen  23790  qtopcld  23851  qtoprest  23855  qtopcmap  23857  kqcldsat  23871  regr1lem  23877  trufil  24048  ufildr  24069  opnsubg  24246  cldsubg  24249  blcld  24643  lebnumlem1  25101  bcthlem1  25464  bcth  25469  bcth3  25471  difmbl  25683  itg1val  25823  itgioo  25956  limciun  26034  dvfval  26037  newval  28009  noxpordpred  28127  istrkgl  28708  ishpg  29022  tgplnfn  29038  plngval  29040  isplng  29041  plng3p  29060  eengv  29310  elntg  29315  isuhgr  29391  isushgr  29392  uhgreq12g  29396  isuhgrop  29401  uhgr0vb  29403  uhgrun  29405  uhgrstrrepe  29409  isupgr  29415  upgrop  29425  isumgr  29426  upgrun  29449  isuspgr  29483  isusgr  29484  isuspgrop  29492  nb3grprlem2  29712  uvtxval  29718  nbupgruvtxres  29738  cplgrop  29768  cusgrexi  29774  structtocusgr  29777  1loopgrnb0  29833  cyclnumvtx  30130  isconngr1  30522  frgr3v  30607  difuncomp  32879  imadifxp  32927  fresunsn  32951  fressupp  33014  supppreima  33017  mptiffisupp  33019  gtiso  33027  difico  33109  fzdif2  33116  fzodif2  33117  fzodif1  33118  nn0diffz0  33120  pmtrcnel2  33391  cycpmconjvlem  33442  cycpmrn  33444  tocyccntz  33445  submarchi  33487  elrgspnlem4  33546  fracfld  33610  elrspunidl  33717  psrbasfsupp  33882  qtophaus  34207  imambfm  34633  difelcarsg  34681  carsgclctunlem1  34688  carsggect  34689  issibf  34704  sibf0  34705  sitgfval  34712  ballotlemfval  34861  ballotlemfp1  34863  ballotlemgun  34896  hgt750lemb  35024  kur14  35689  iscvm  35732  cvmscld  35746  satf  35826  mdvval  35977  topbnd  36816  pibp21  38042  poimirlem2  38254  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem11  38263  poimirlem12  38264  poimirlem13  38265  poimirlem14  38266  poimirlem16  38268  poimirlem18  38270  poimirlem19  38271  poimirlem21  38273  poimirlem22  38274  poimirlem23  38275  poimirlem27  38279  poimirlem30  38282  mblfinlem3  38291  mblfinlem4  38292  itg2addnclem  38303  itg2addnclem2  38304  prjspeclsp  43327  aomclem8  43771  kelac2  43775  gneispace2  44841  fzdifsuc2  46012  iccdifioo  46214  iccdifprioo  46215  ibliooicc  46668  dirkercncflem2  46801  issal  47011  prsal  47015  saldifcl2  47025  intsal  47027  sge0fodjrnlem  47113  caratheodorylem1  47223  vonvolmbllem  47357  salpreimagelt  47404  salpreimalegt  47406  smfresal  47485  chnsubseq  47579  dfnbgr5  48599  dfnbgr6  48605  isubgruhgr  48616  stgrnbgr0  48712  lines  49494  rrxlines  49496  eenglngeehlnm  49502  clddisj  49665  iscnrm3rlem1  49701