Theorem difeq1i 4058

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

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4046

This theorem is used by:  difeq12i  4060  dfin3  4221  indif1  4226  indifcom  4227  difun1  4243  notab  4258  rabdif  4265  notrab  4266  undifabs  4433  difprsn1  4759  difprsn2  4760  diftpsn3  4761  resdifcom  5989  resdmdfsn  6022  resdmdfsnOLD  6023  frpoind  6347  orddif  6463  fresaun  6756  f12dfv  7283  f13dfv  7284  domunsncan  9101  elfiun  9427  frind  9759  dju1dif  10256  axcclem  10540  dfn2  12624  nulchn  18800  s1chn  18801  chnccat  18807  ex-chn1  18818  ex-chn2  18819  mvdco  19666  pmtrdifellem2  19698  islinds2  22126  lindsind2  22132  lindsenlbs  22164  restcld  23497  ufprim  24235  volun  25873  itgsplitioo  26165  uhgr0vb  29657  uhgr0  29658  uvtxupgrres  29996  cplgr3v  30023  ex-dif  31031  indifundif  33169  imadifxp  33244  aciunf1  33306  indsupp  33482  pmtrcnelor  33700  lindsunlem  34304  lindsun  34305  braew  34923  carsgclctunlem1  34997  carsggect  34998  coinflippvt  35165  ballotlemfval0  35176  signstfvcl  35250  acwer1prc  35818  satf0  36225  onint1  37331  bj-2upln1upl  38031  bj-disj2r  38035  poimirlem13  38658  poimirlem14  38659  poimirlem18  38663  poimirlem21  38666  poimirlem30  38675  itg2addnclem  38696  asindmre  38728  disjresundif  39285  dmxrnuncnvepres  39431  dmxrncnvepres2  39472  sucdifsn  39525  ressucdifsn  39527  kelac2  44174  fourierdlem102  47325  fourierdlem114  47337  pwsal  47432  issald  47450  sge0fodjrnlem  47533  hoiprodp1  47705  lincext2  49674  disjdifb  50027