Theorem difeq1i 4081

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

Syntax hints:   = wceq 1540   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-dif 3914

This theorem is referenced by:  difeq12i  4083  dfin3  4236  indif1  4241  indifcom  4242  difun1  4258  notab  4273  rabdif  4280  notrab  4281  undifabs  4437  difprsn1  4760  difprsn2  4761  diftpsn3  4762  resdifcom  5958  resdmdfsn  5991  frpoind  6303  orddif  6418  fresaun  6713  f12dfv  7230  f13dfv  7231  domunsncan  9018  elfiun  9357  frind  9679  dju1dif  10102  axcclem  10386  dfn2  12431  mvdco  19351  pmtrdifellem2  19383  islinds2  21698  lindsind2  21704  restcld  23035  ufprim  23772  volun  25422  itgsplitioo  25715  uhgr0vb  28975  uhgr0  28976  uvtxupgrres  29311  cplgr3v  29338  ex-dif  30325  indifundif  32426  imadifxp  32503  aciunf1  32560  indsupp  32763  s1chn  32909  pmtrcnelor  33021  lindsunlem  33593  lindsun  33594  braew  34205  carsgclctunlem1  34281  carsggect  34282  coinflippvt  34449  ballotlemfval0  34460  signstfvcl  34537  satf0  35332  onint1  36410  bj-2upln1upl  36985  bj-disj2r  36989  lindsenlbs  37582  poimirlem13  37600  poimirlem14  37601  poimirlem18  37605  poimirlem21  37608  poimirlem30  37617  itg2addnclem  37638  asindmre  37670  sucdifsn  38200  disjresundif  38204  ressucdifsn  38206  kelac2  43027  fourierdlem102  46179  fourierdlem114  46191  pwsal  46286  issald  46304  sge0fodjrnlem  46387  hoiprodp1  46559  lincext2  48417  disjdifb  48771