Theorem difeq1i 4083

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

Syntax hints:   = wceq 1541   ∖ cdif 3910

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-dif 3916

This theorem is referenced by:  difeq12i  4085  dfin3  4231  indif1  4236  indifcom  4237  difun1  4254  notab  4269  notrab  4276  undifabs  4442  difprsn1  4765  difprsn2  4766  diftpsn3  4767  resdifcom  5961  resdmdfsn  5992  frpoind  6301  wfiOLD  6310  orddif  6418  fresaun  6718  f12dfv  7224  f13dfv  7225  domunsncan  9023  phplem1OLD  9168  elfiun  9375  frind  9695  dju1dif  10117  axcclem  10402  dfn2  12435  mvdco  19241  pmtrdifellem2  19273  islinds2  21256  lindsind2  21262  restcld  22560  ufprim  23297  volun  24946  itgsplitioo  25239  uhgr0vb  28086  uhgr0  28087  uvtxupgrres  28419  cplgr3v  28446  ex-dif  29430  indifundif  31516  imadifxp  31586  aciunf1  31646  pmtrcnelor  32012  lindsunlem  32406  lindsun  32407  braew  32930  carsgclctunlem1  33006  carsggect  33007  coinflippvt  33173  ballotlemfval0  33184  signstfvcl  33274  satf0  34053  onint1  34997  bj-2upln1upl  35568  bj-disj2r  35572  lindsenlbs  36146  poimirlem13  36164  poimirlem14  36165  poimirlem18  36169  poimirlem21  36172  poimirlem30  36181  itg2addnclem  36202  asindmre  36234  sucdifsn  36769  disjresundif  36773  ressucdifsn  36775  rabdif  40708  kelac2  41450  fourierdlem102  44569  fourierdlem114  44581  pwsal  44676  issald  44694  sge0fodjrnlem  44777  hoiprodp1  44949  lincext2  46656  disjdifb  47014