Theorem difeq1d 4098

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

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

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-dif 3939

This theorem is referenced by:  difeq12d  4100  dffv2  6756  phplem4  8699  unfilem3  8784  marypha1lem  8897  infdifsn  9120  cantnfp1lem3  9143  en2other2  9435  isacn  9470  fin23lem28  9762  enfin1ai  9806  fin1a2lem7  9828  fzdifsuc  12968  axdc4uz  13353  leiso  13818  cshimadifsn  14191  isstruct2  16493  setsfun0  16519  strle1  16592  pltfval  17569  f1omvdco2  18576  symgsssg  18595  symgfisg  18596  symggen  18598  pmtrdifellem3  18606  pmtrdifwrdellem3  18611  pmtrdifwrdel2lem1  18612  pmtrdifwrdel  18613  pmtrdifwrdel2  18614  psgnunilem1  18621  psgnunilem5  18622  psgnunilem2  18623  psgnunilem3  18624  gsumval3  19027  dmdprd  19120  dprd2da  19164  dmdprdsplit2lem  19167  dpjfval  19177  ablfac1eulem  19194  subdrgint  19582  lssset  19705  lbspropd  19871  opsrtoslem2  20265  islindf  20956  islindf2  20958  f1lindf  20966  cldval  21631  difopn  21642  mretopd  21700  restcld  21780  ordtcld1  21805  ordtcld2  21806  cnclima  21876  iscncl  21877  isreg2  21985  llycmpkgen2  22158  1stckgen  22162  ptval  22178  txcld  22211  ptcld  22221  txkgen  22260  qtopcld  22321  qtoprest  22325  qtopcmap  22327  kqcldsat  22341  regr1lem  22347  trufil  22518  ufildr  22539  opnsubg  22716  cldsubg  22719  blcld  23115  lebnumlem1  23565  bcthlem1  23927  bcth  23932  bcth3  23934  difmbl  24144  itg1val  24284  itgioo  24416  limciun  24492  dvfval  24495  istrkgl  26244  ishpg  26545  eengv  26765  elntg  26770  isuhgr  26845  isushgr  26846  uhgreq12g  26850  isuhgrop  26855  uhgr0vb  26857  uhgrun  26859  uhgrstrrepe  26863  isupgr  26869  upgrop  26879  isumgr  26880  upgrun  26903  isuspgr  26937  isusgr  26938  isuspgrop  26946  nb3grprlem2  27163  uvtxval  27169  nbupgruvtxres  27189  cplgrop  27219  cusgrexi  27225  structtocusgr  27228  1loopgrnb0  27284  isconngr1  27969  frgr3v  28054  difuncomp  30305  imadifxp  30351  gtiso  30436  difico  30506  fzdif2  30514  fzodif2  30515  fzodif1  30516  pmtrcnel2  30734  cycpmconjvlem  30783  cycpmrn  30785  tocyccntz  30786  submarchi  30815  qtophaus  31100  imambfm  31520  difelcarsg  31568  carsgclctunlem1  31575  carsggect  31576  issibf  31591  sibf0  31592  sitgfval  31599  ballotlemfval  31747  ballotlemfp1  31749  ballotlemgun  31782  hgt750lemb  31927  kur14  32463  iscvm  32506  cvmscld  32520  satf  32600  mdvval  32751  topbnd  33672  pibp21  34699  poimirlem2  34909  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem16  34923  poimirlem18  34925  poimirlem19  34926  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem27  34934  poimirlem30  34937  mblfinlem3  34946  mblfinlem4  34947  itg2addnclem  34958  itg2addnclem2  34959  prjspeclsp  39311  aomclem8  39710  kelac2  39714  gneispace2  40531  fzdifsuc2  41626  iccdifioo  41840  iccdifprioo  41841  ibliooicc  42305  dirkercncflem2  42438  issal  42648  prsal  42652  saldifcl2  42660  intsal  42662  sge0fodjrnlem  42747  caratheodorylem1  42857  vonvolmbllem  42991  salpreimagelt  43035  salpreimalegt  43037  smfresal  43112  lines  44767  rrxlines  44769  eenglngeehlnm  44775