Theorem difeq1d 4100

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

Syntax hints:   → wi 4   = wceq 1537   ∖ cdif 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149  df-dif 3941

This theorem is referenced by:  difeq12d  4102  dffv2  6758  phplem4  8701  unfilem3  8786  marypha1lem  8899  infdifsn  9122  cantnfp1lem3  9145  en2other2  9437  isacn  9472  fin23lem28  9764  enfin1ai  9808  fin1a2lem7  9830  fzdifsuc  12970  axdc4uz  13355  leiso  13820  cshimadifsn  14193  isstruct2  16495  setsfun0  16521  strle1  16594  pltfval  17571  f1omvdco2  18578  symgsssg  18597  symgfisg  18598  symggen  18600  pmtrdifellem3  18608  pmtrdifwrdellem3  18613  pmtrdifwrdel2lem1  18614  pmtrdifwrdel  18615  pmtrdifwrdel2  18616  psgnunilem1  18623  psgnunilem5  18624  psgnunilem2  18625  psgnunilem3  18626  gsumval3  19029  dmdprd  19122  dprd2da  19166  dmdprdsplit2lem  19169  dpjfval  19179  ablfac1eulem  19196  subdrgint  19584  lssset  19707  lbspropd  19873  opsrtoslem2  20267  islindf  20958  islindf2  20960  f1lindf  20968  cldval  21633  difopn  21644  mretopd  21702  restcld  21782  ordtcld1  21807  ordtcld2  21808  cnclima  21878  iscncl  21879  isreg2  21987  llycmpkgen2  22160  1stckgen  22164  ptval  22180  txcld  22213  ptcld  22223  txkgen  22262  qtopcld  22323  qtoprest  22327  qtopcmap  22329  kqcldsat  22343  regr1lem  22349  trufil  22520  ufildr  22541  opnsubg  22718  cldsubg  22721  blcld  23117  lebnumlem1  23567  bcthlem1  23929  bcth  23934  bcth3  23936  difmbl  24146  itg1val  24286  itgioo  24418  limciun  24494  dvfval  24497  istrkgl  26246  ishpg  26547  eengv  26767  elntg  26772  isuhgr  26847  isushgr  26848  uhgreq12g  26852  isuhgrop  26857  uhgr0vb  26859  uhgrun  26861  uhgrstrrepe  26865  isupgr  26871  upgrop  26881  isumgr  26882  upgrun  26905  isuspgr  26939  isusgr  26940  isuspgrop  26948  nb3grprlem2  27165  uvtxval  27171  nbupgruvtxres  27191  cplgrop  27221  cusgrexi  27227  structtocusgr  27230  1loopgrnb0  27286  isconngr1  27971  frgr3v  28056  difuncomp  30307  imadifxp  30353  gtiso  30438  difico  30508  fzdif2  30516  fzodif2  30517  fzodif1  30518  pmtrcnel2  30736  cycpmconjvlem  30785  cycpmrn  30787  tocyccntz  30788  submarchi  30817  qtophaus  31102  imambfm  31522  difelcarsg  31570  carsgclctunlem1  31577  carsggect  31578  issibf  31593  sibf0  31594  sitgfval  31601  ballotlemfval  31749  ballotlemfp1  31751  ballotlemgun  31784  hgt750lemb  31929  kur14  32465  iscvm  32508  cvmscld  32522  satf  32602  mdvval  32753  topbnd  33674  pibp21  34698  poimirlem2  34896  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem16  34910  poimirlem18  34912  poimirlem19  34913  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem27  34921  poimirlem30  34924  mblfinlem3  34933  mblfinlem4  34934  itg2addnclem  34945  itg2addnclem2  34946  prjspeclsp  39269  aomclem8  39668  kelac2  39672  gneispace2  40489  fzdifsuc2  41584  iccdifioo  41798  iccdifprioo  41799  ibliooicc  42263  dirkercncflem2  42396  issal  42606  prsal  42610  saldifcl2  42618  intsal  42620  sge0fodjrnlem  42705  caratheodorylem1  42815  vonvolmbllem  42949  salpreimagelt  42993  salpreimalegt  42995  smfresal  43070  lines  44725  rrxlines  44727  eenglngeehlnm  44733