Theorem difeq1i 4046

Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
difeq1i	⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Proof of Theorem difeq1i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		difeq1 4043	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Syntax hints:   = wceq 1538   ∖ cdif 3878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-dif 3884

This theorem is referenced by:  difeq12i  4048  dfin3  4193  indif1  4198  indifcom  4199  difun1  4214  notab  4225  notrab  4232  undifabs  4384  difprsn1  4693  difprsn2  4694  diftpsn3  4695  resdifcom  5837  resdmdfsn  5868  wfi  6149  orddif  6252  fresaun  6523  f12dfv  7008  f13dfv  7009  domunsncan  8600  phplem1  8680  elfiun  8878  dju1dif  9583  axcclem  9868  dfn2  11898  mvdco  18565  pmtrdifellem2  18597  islinds2  20502  lindsind2  20508  restcld  21777  ufprim  22514  volun  24149  itgsplitioo  24441  uhgr0vb  26865  uhgr0  26866  uvtxupgrres  27198  cplgr3v  27225  ex-dif  28208  indifundif  30297  imadifxp  30364  aciunf1  30426  pmtrcnelor  30785  lindsunlem  31108  lindsun  31109  braew  31611  carsgclctunlem1  31685  carsggect  31686  coinflippvt  31852  ballotlemfval0  31863  signstfvcl  31953  satf0  32732  frpoind  33193  frind  33198  onint1  33910  bj-2upln1upl  34460  bj-disj2r  34464  lindsenlbs  35052  poimirlem13  35070  poimirlem14  35071  poimirlem18  35075  poimirlem21  35078  poimirlem30  35087  itg2addnclem  35108  asindmre  35140  rabdif  39399  kelac2  40009  fourierdlem102  42850  fourierdlem114  42862  pwsal  42957  issald  42973  sge0fodjrnlem  43055  hoiprodp1  43227  lincext2  44864