Theorem difeq1i 4131

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 4128	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∖ 𝐶) = (𝐵 ∖ 𝐶)

Syntax hints:   = wceq 1536   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-dif 3965

This theorem is referenced by:  difeq12i  4133  dfin3  4282  indif1  4287  indifcom  4288  difun1  4304  notab  4319  rabdif  4326  notrab  4327  undifabs  4483  difprsn1  4804  difprsn2  4805  diftpsn3  4806  resdifcom  6018  resdmdfsn  6050  frpoind  6364  wfiOLD  6373  orddif  6481  fresaun  6779  f12dfv  7292  f13dfv  7293  domunsncan  9110  phplem1OLD  9251  elfiun  9467  frind  9787  dju1dif  10210  axcclem  10494  dfn2  12536  mvdco  19477  pmtrdifellem2  19509  islinds2  21850  lindsind2  21856  restcld  23195  ufprim  23932  volun  25593  itgsplitioo  25887  uhgr0vb  29103  uhgr0  29104  uvtxupgrres  29439  cplgr3v  29466  ex-dif  30451  indifundif  32551  imadifxp  32620  aciunf1  32679  pmtrcnelor  33093  lindsunlem  33651  lindsun  33652  braew  34222  carsgclctunlem1  34298  carsggect  34299  coinflippvt  34465  ballotlemfval0  34476  signstfvcl  34566  satf0  35356  onint1  36431  bj-2upln1upl  37006  bj-disj2r  37010  lindsenlbs  37601  poimirlem13  37619  poimirlem14  37620  poimirlem18  37624  poimirlem21  37627  poimirlem30  37636  itg2addnclem  37657  asindmre  37689  sucdifsn  38219  disjresundif  38223  ressucdifsn  38225  kelac2  43053  fourierdlem102  46163  fourierdlem114  46175  pwsal  46270  issald  46288  sge0fodjrnlem  46371  hoiprodp1  46543  lincext2  48300  disjdifb  48657