Theorem difeq1d 4063

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

Syntax hints:   → wi 4   = wceq 1547   ∖ cdif 3887

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-dif 3893

This theorem is referenced by:  difeq12d  4065  dffv2  6929  on2recsov  8601  phplem2  9136  unfilem3  9214  marypha1lem  9343  infdifsn  9576  cantnfp1lem3  9599  en2other2  9929  isacn  9964  fin23lem28  10260  enfin1ai  10304  fin1a2lem7  10326  fzdifsuc  13536  axdc4uz  13944  leiso  14419  cshimadifsn  14789  isstruct2  17117  strle1  17126  setsfun0  17140  pltfval  18293  ischn  18571  chnind  18585  chnccats1  18589  chnccat  18590  f1omvdco2  19421  symgsssg  19440  symgfisg  19441  symggen  19443  pmtrdifellem3  19451  pmtrdifwrdellem3  19456  pmtrdifwrdel2lem1  19457  pmtrdifwrdel  19458  pmtrdifwrdel2  19459  psgnunilem1  19466  psgnunilem5  19467  psgnunilem2  19468  psgnunilem3  19469  gsumval3  19880  dmdprd  19973  dprd2da  20017  dmdprdsplit2lem  20020  dpjfval  20030  ablfac1eulem  20047  subdrgint  20782  lssset  20930  lbspropd  21096  islindf  21794  islindf2  21796  f1lindf  21804  opsrtoslem2  22039  cldval  23013  difopn  23024  mretopd  23082  restcld  23162  ordtcld1  23187  ordtcld2  23188  cnclima  23258  iscncl  23259  isreg2  23367  llycmpkgen2  23540  1stckgen  23544  ptval  23560  txcld  23593  ptcld  23603  txkgen  23642  qtopcld  23703  qtoprest  23707  qtopcmap  23709  kqcldsat  23723  regr1lem  23729  trufil  23900  ufildr  23921  opnsubg  24098  cldsubg  24101  blcld  24495  lebnumlem1  24953  bcthlem1  25316  bcth  25321  bcth3  25323  difmbl  25535  itg1val  25675  itgioo  25808  limciun  25886  dvfval  25889  newval  27852  noxpordpred  27970  istrkgl  28551  ishpg  28852  eengv  29073  elntg  29078  isuhgr  29154  isushgr  29155  uhgreq12g  29159  isuhgrop  29164  uhgr0vb  29166  uhgrun  29168  uhgrstrrepe  29172  isupgr  29178  upgrop  29188  isumgr  29189  upgrun  29212  isuspgr  29246  isusgr  29247  isuspgrop  29255  nb3grprlem2  29475  uvtxval  29481  nbupgruvtxres  29501  cplgrop  29531  cusgrexi  29537  structtocusgr  29540  1loopgrnb0  29596  cyclnumvtx  29893  isconngr1  30285  frgr3v  30370  difuncomp  32649  imadifxp  32697  fresunsn  32724  fressupp  32787  supppreima  32790  mptiffisupp  32792  gtiso  32800  difico  32882  fzdif2  32889  fzodif2  32890  fzodif1  32891  nn0diffz0  32893  pmtrcnel2  33178  cycpmconjvlem  33229  cycpmrn  33231  tocyccntz  33232  submarchi  33274  elrgspnlem4  33333  fracfld  33399  elrspunidl  33518  psrbasfsupp  33702  qtophaus  34027  imambfm  34453  difelcarsg  34501  carsgclctunlem1  34508  carsggect  34509  issibf  34524  sibf0  34525  sitgfval  34532  ballotlemfval  34681  ballotlemfp1  34683  ballotlemgun  34716  hgt750lemb  34847  kur14  35451  iscvm  35494  cvmscld  35508  satf  35588  mdvval  35739  topbnd  36559  pibp21  37784  poimirlem2  37996  poimirlem4  37998  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem14  38008  poimirlem16  38010  poimirlem18  38012  poimirlem19  38013  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem27  38021  poimirlem30  38024  mblfinlem3  38033  mblfinlem4  38034  itg2addnclem  38045  itg2addnclem2  38046  prjspeclsp  43069  aomclem8  43513  kelac2  43517  gneispace2  44583  fzdifsuc2  45765  iccdifioo  45967  iccdifprioo  45968  ibliooicc  46421  dirkercncflem2  46554  issal  46764  prsal  46768  saldifcl2  46778  intsal  46780  sge0fodjrnlem  46866  caratheodorylem1  46976  vonvolmbllem  47110  salpreimagelt  47157  salpreimalegt  47159  smfresal  47238  chnsubseq  47332  dfnbgr5  48349  dfnbgr6  48355  isubgruhgr  48366  stgrnbgr0  48462  lines  49229  rrxlines  49231  eenglngeehlnm  49237  clddisj  49401  iscnrm3rlem1  49437