Theorem difeq1i 4062

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  difeq12i  4064  dfin3  4225  indif1  4230  indifcom  4231  difun1  4247  notab  4262  rabdif  4269  notrab  4270  undifabs  4437  difprsn1  4765  difprsn2  4766  diftpsn3  4767  resdifcom  6005  resdmdfsn  6039  resdmdfsnOLD  6040  frpoind  6371  orddif  6487  fresaun  6783  f12dfv  7312  f13dfv  7313  domunsncan  9134  elfiun  9459  frind  9791  dju1dif  10290  axcclem  10574  dfn2  12659  nulchn  18843  s1chn  18844  chnccat  18850  ex-chn1  18861  ex-chn2  18862  mvdco  19710  pmtrdifellem2  19742  islinds2  22174  lindsind2  22180  lindsenlbs  22212  restcld  23545  ufprim  24283  volun  25921  itgsplitioo  26213  uhgr0vb  29707  uhgr0  29708  uvtxupgrres  30046  cplgr3v  30073  ex-dif  31081  indifundif  33219  imadifxp  33293  aciunf1  33355  indsupp  33530  pmtrcnelor  33751  lindsunlem  34367  lindsun  34368  braew  34986  carsgclctunlem1  35060  carsggect  35061  coinflippvt  35228  ballotlemfval0  35239  signstfvcl  35313  acwer1prc  35893  satf0  36345  onint1  37452  bj-2upln1upl  38152  bj-disj2r  38156  poimirlem13  38819  poimirlem14  38820  poimirlem18  38824  poimirlem21  38827  poimirlem30  38836  itg2addnclem  38857  asindmre  38889  disjresundif  39444  dmxrnuncnvepres  39590  dmxrncnvepres2  39631  sucdifsn  39684  ressucdifsn  39686  kelac2  44333  fourierdlem102  47491  fourierdlem114  47503  pwsal  47598  issald  47616  sge0fodjrnlem  47699  hoiprodp1  47871  lincext2  49898  disjdifb  50251