Theorem difeq1i 3686

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

Syntax hints:   = wceq 1475   ∖ cdif 3537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-dif 3543

This theorem is referenced by:  difeq12i  3688  dfin3  3825  indif1  3830  indifcom  3831  difun1  3846  notab  3856  notrab  3863  undifabs  3997  difprsn1  4271  difprsn2  4272  diftpsn3  4273  resdifcom  5335  resdmdfsn  5365  wfi  5630  orddif  5737  fresaun  5988  f12dfv  6429  f13dfv  6430  domunsncan  7945  phplem1  8024  elfiun  8219  axcclem  9162  dfn2  11182  mvdco  17688  pmtrdifellem2  17720  islinds2  19971  lindsind2  19977  restcld  20786  ufprim  21523  volun  23120  itgsplitioo  23410  uhgr0vb  25738  uhgr0  25739  uhgra0v  25839  usgra0v  25900  usgra1v  25919  cusgra3v  25993  ex-dif  26672  indifundif  28740  imadifxp  28796  aciunf1  28845  braew  29632  carsgclctunlem1  29706  carsggect  29707  coinflippvt  29873  ballotlemfval0  29884  signstfvcl  29976  frind  30984  onint1  31618  bj-2upln1upl  32205  lindsenlbs  32574  poimirlem13  32592  poimirlem14  32593  poimirlem18  32597  poimirlem21  32600  poimirlem30  32609  itg2addnclem  32631  asindmre  32665  kelac2  36653  fourierdlem102  39101  fourierdlem114  39113  pwsal  39211  issald  39227  sge0fodjrnlem  39309  hoiprodp1  39478  uvtxupgrres  40635  cplgr3v  40657  konigsbergiedgwOLD  41417  lincext2  42038