Theorem difeq1i 4085

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

Syntax hints:   = wceq 1540   ∖ cdif 3911

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 3406  df-dif 3917

This theorem is referenced by:  difeq12i  4087  dfin3  4240  indif1  4245  indifcom  4246  difun1  4262  notab  4277  rabdif  4284  notrab  4285  undifabs  4441  difprsn1  4764  difprsn2  4765  diftpsn3  4766  resdifcom  5969  resdmdfsn  6002  frpoind  6315  orddif  6430  fresaun  6731  f12dfv  7248  f13dfv  7249  domunsncan  9041  elfiun  9381  frind  9703  dju1dif  10126  axcclem  10410  dfn2  12455  mvdco  19375  pmtrdifellem2  19407  islinds2  21722  lindsind2  21728  restcld  23059  ufprim  23796  volun  25446  itgsplitioo  25739  uhgr0vb  28999  uhgr0  29000  uvtxupgrres  29335  cplgr3v  29362  ex-dif  30352  indifundif  32453  imadifxp  32530  aciunf1  32587  indsupp  32790  s1chn  32936  pmtrcnelor  33048  lindsunlem  33620  lindsun  33621  braew  34232  carsgclctunlem1  34308  carsggect  34309  coinflippvt  34476  ballotlemfval0  34487  signstfvcl  34564  satf0  35359  onint1  36437  bj-2upln1upl  37012  bj-disj2r  37016  lindsenlbs  37609  poimirlem13  37627  poimirlem14  37628  poimirlem18  37632  poimirlem21  37635  poimirlem30  37644  itg2addnclem  37665  asindmre  37697  sucdifsn  38227  disjresundif  38231  ressucdifsn  38233  kelac2  43054  fourierdlem102  46206  fourierdlem114  46218  pwsal  46313  issald  46331  sge0fodjrnlem  46414  hoiprodp1  46586  lincext2  48444  disjdifb  48798