Theorem difeq1i 4077

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-dif 3909

This theorem is used by:  difeq12i  4079  dfin3  4230  indif1  4235  indifcom  4236  difun1  4252  notab  4267  rabdif  4274  notrab  4275  undifabs  4441  difprsn1  4770  difprsn2  4771  diftpsn3  4772  resdifcom  5999  resdmdfsn  6033  resdmdfsnOLD  6034  frpoind  6347  orddif  6463  fresaun  6753  f12dfv  7277  f13dfv  7278  domunsncan  9068  elfiun  9393  frind  9725  dju1dif  10168  axcclem  10452  dfn2  12528  nulchn  18693  s1chn  18694  chnccat  18700  ex-chn1  18711  ex-chn2  18712  mvdco  19539  pmtrdifellem2  19571  islinds2  21993  lindsind2  21999  restcld  23359  ufprim  24097  volun  25735  itgsplitioo  26028  uhgr0vb  29453  uhgr0  29454  uvtxupgrres  29792  cplgr3v  29819  ex-dif  30821  indifundif  32917  imadifxp  32993  aciunf1  33055  indsupp  33233  pmtrcnelor  33451  lindsunlem  34054  lindsun  34055  braew  34673  carsgclctunlem1  34748  carsggect  34749  coinflippvt  34916  ballotlemfval0  34927  signstfvcl  35001  satf0  35877  onint1  36993  bj-2upln1upl  37693  bj-disj2r  37697  lindsenlbs  38299  poimirlem13  38317  poimirlem14  38318  poimirlem18  38322  poimirlem21  38325  poimirlem30  38334  itg2addnclem  38355  asindmre  38387  disjresundif  38928  dmxrnuncnvepres  39074  dmxrncnvepres2  39115  sucdifsn  39168  ressucdifsn  39170  kelac2  43825  fourierdlem102  46955  fourierdlem114  46967  pwsal  47062  issald  47080  sge0fodjrnlem  47163  hoiprodp1  47335  lincext2  49268  disjdifb  49621