Theorem difeq1d 3988

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

Syntax hints:   → wi 4   = wceq 1507   ∖ cdif 3826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-rab 3097  df-dif 3832

This theorem is referenced by:  difeq12d  3990  dffv2  6584  phplem4  8495  unfilem3  8579  marypha1lem  8692  infdifsn  8914  cantnfp1lem3  8937  en2other2  9229  isacn  9264  fin23lem28  9560  enfin1ai  9604  fin1a2lem7  9626  fzdifsuc  12783  axdc4uz  13167  leiso  13630  cshimadifsn  14053  isstruct2  16349  setsfun0  16375  strle1  16448  pltfval  17427  f1omvdco2  18337  symgsssg  18356  symgfisg  18357  symggen  18359  pmtrdifellem3  18367  pmtrdifwrdellem3  18372  pmtrdifwrdel2lem1  18373  pmtrdifwrdel  18374  pmtrdifwrdel2  18375  psgnunilem1  18382  psgnunilem5  18383  psgnunilem5OLD  18384  psgnunilem2  18385  psgnunilem3  18386  gsumval3  18781  dmdprd  18870  dprd2da  18914  dmdprdsplit2lem  18917  dpjfval  18927  ablfac1eulem  18944  subdrgint  19304  lssset  19427  lbspropd  19593  opsrtoslem2  19978  islindf  20658  islindf2  20660  f1lindf  20668  cldval  21335  difopn  21346  mretopd  21404  restcld  21484  ordtcld1  21509  ordtcld2  21510  cnclima  21580  iscncl  21581  isreg2  21689  llycmpkgen2  21862  1stckgen  21866  ptval  21882  txcld  21915  ptcld  21925  txkgen  21964  qtopcld  22025  qtoprest  22029  qtopcmap  22031  kqcldsat  22045  regr1lem  22051  trufil  22222  ufildr  22243  opnsubg  22419  cldsubg  22422  blcld  22818  lebnumlem1  23268  bcthlem1  23630  bcth  23635  bcth3  23637  difmbl  23847  itg1val  23987  itgioo  24119  limciun  24195  dvfval  24198  istrkgl  25946  ishpg  26247  eengv  26468  elntg  26473  isuhgr  26548  isushgr  26549  uhgreq12g  26553  isuhgrop  26558  uhgr0vb  26560  uhgrun  26562  uhgrstrrepe  26566  isupgr  26572  upgrop  26582  isumgr  26583  upgrun  26606  isuspgr  26640  isusgr  26641  isuspgrop  26649  nb3grprlem2  26866  uvtxval  26872  nbupgruvtxres  26892  cplgrop  26922  cusgrexi  26928  structtocusgr  26931  1loopgrnb0  26987  isconngr1  27719  isfrgr  27792  frgr3v  27809  difuncomp  30073  imadifxp  30117  gtiso  30195  difico  30265  fzdif2  30271  fzodif2  30272  submarchi  30487  qtophaus  30750  imambfm  31171  difelcarsg  31219  carsgclctunlem1  31226  carsggect  31227  issibf  31242  sibf0  31243  sitgfval  31250  ballotlemfval  31399  ballotlemfp1  31401  ballotlemgun  31434  hgt750lemb  31581  kur14  32054  iscvm  32097  cvmscld  32111  satf  32187  mdvval  32277  topbnd  33199  pibp21  34143  poimirlem2  34341  poimirlem4  34343  poimirlem6  34345  poimirlem7  34346  poimirlem8  34347  poimirlem11  34350  poimirlem12  34351  poimirlem13  34352  poimirlem14  34353  poimirlem16  34355  poimirlem18  34357  poimirlem19  34358  poimirlem21  34360  poimirlem22  34361  poimirlem23  34362  poimirlem27  34366  poimirlem30  34369  mblfinlem3  34378  mblfinlem4  34379  itg2addnclem  34390  itg2addnclem2  34391  prjspeclsp  38675  aomclem8  39063  kelac2  39067  gneispace2  39851  fzdifsuc2  41012  iccdifioo  41228  iccdifprioo  41229  ibliooicc  41692  dirkercncflem2  41826  issal  42036  prsal  42040  saldifcl2  42048  intsal  42050  sge0fodjrnlem  42135  caratheodorylem1  42245  vonvolmbllem  42379  salpreimagelt  42423  salpreimalegt  42425  smfresal  42500  lines  44092  rrxlines  44094  eenglngeehlnm  44100