Theorem difeq1d 4120

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

Syntax hints:   → wi 4   = wceq 1539   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-dif 3950

This theorem is referenced by:  difeq12d  4122  dffv2  6985  on2recsov  8669  phplem2  9210  phplem4OLD  9222  unfilem3  9314  marypha1lem  9430  infdifsn  9654  cantnfp1lem3  9677  en2other2  10006  isacn  10041  fin23lem28  10337  enfin1ai  10381  fin1a2lem7  10403  fzdifsuc  13565  axdc4uz  13953  leiso  14424  cshimadifsn  14784  isstruct2  17086  strle1  17095  setsfun0  17109  pltfval  18288  f1omvdco2  19357  symgsssg  19376  symgfisg  19377  symggen  19379  pmtrdifellem3  19387  pmtrdifwrdellem3  19392  pmtrdifwrdel2lem1  19393  pmtrdifwrdel  19394  pmtrdifwrdel2  19395  psgnunilem1  19402  psgnunilem5  19403  psgnunilem2  19404  psgnunilem3  19405  gsumval3  19816  dmdprd  19909  dprd2da  19953  dmdprdsplit2lem  19956  dpjfval  19966  ablfac1eulem  19983  subdrgint  20562  lssset  20688  lbspropd  20854  islindf  21586  islindf2  21588  f1lindf  21596  opsrtoslem2  21836  cldval  22747  difopn  22758  mretopd  22816  restcld  22896  ordtcld1  22921  ordtcld2  22922  cnclima  22992  iscncl  22993  isreg2  23101  llycmpkgen2  23274  1stckgen  23278  ptval  23294  txcld  23327  ptcld  23337  txkgen  23376  qtopcld  23437  qtoprest  23441  qtopcmap  23443  kqcldsat  23457  regr1lem  23463  trufil  23634  ufildr  23655  opnsubg  23832  cldsubg  23835  blcld  24234  lebnumlem1  24707  bcthlem1  25072  bcth  25077  bcth3  25079  difmbl  25292  itg1val  25432  itgioo  25565  limciun  25643  dvfval  25646  newval  27587  noxpordpred  27675  istrkgl  27976  ishpg  28277  eengv  28504  elntg  28509  isuhgr  28587  isushgr  28588  uhgreq12g  28592  isuhgrop  28597  uhgr0vb  28599  uhgrun  28601  uhgrstrrepe  28605  isupgr  28611  upgrop  28621  isumgr  28622  upgrun  28645  isuspgr  28679  isusgr  28680  isuspgrop  28688  nb3grprlem2  28905  uvtxval  28911  nbupgruvtxres  28931  cplgrop  28961  cusgrexi  28967  structtocusgr  28970  1loopgrnb0  29026  isconngr1  29710  frgr3v  29795  difuncomp  32052  imadifxp  32099  fressupp  32177  supppreima  32180  mptiffisupp  32182  gtiso  32189  difico  32261  fzdif2  32269  fzodif2  32270  fzodif1  32271  pmtrcnel2  32521  cycpmconjvlem  32570  cycpmrn  32572  tocyccntz  32573  submarchi  32602  elrspunidl  32820  qtophaus  33114  imambfm  33559  difelcarsg  33607  carsgclctunlem1  33614  carsggect  33615  issibf  33630  sibf0  33631  sitgfval  33638  ballotlemfval  33786  ballotlemfp1  33788  ballotlemgun  33821  hgt750lemb  33966  kur14  34505  iscvm  34548  cvmscld  34562  satf  34642  mdvval  34793  topbnd  35512  pibp21  36599  poimirlem2  36793  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem11  36802  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem16  36807  poimirlem18  36809  poimirlem19  36810  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem27  36818  poimirlem30  36821  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem  36842  itg2addnclem2  36843  prjspeclsp  41656  aomclem8  42105  kelac2  42109  gneispace2  43185  fzdifsuc2  44318  iccdifioo  44526  iccdifprioo  44527  ibliooicc  44985  dirkercncflem2  45118  issal  45328  prsal  45332  saldifcl2  45342  intsal  45344  sge0fodjrnlem  45430  caratheodorylem1  45540  vonvolmbllem  45674  salpreimagelt  45721  salpreimalegt  45723  smfresal  45802  lines  47504  rrxlines  47506  eenglngeehlnm  47512  clddisj  47623  iscnrm3rlem1  47660