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  7280  f13dfv  7281  domunsncan  9072  elfiun  9397  frind  9729  dju1dif  10172  axcclem  10456  dfn2  12532  nulchn  18697  s1chn  18698  chnccat  18704  ex-chn1  18715  ex-chn2  18716  mvdco  19559  pmtrdifellem2  19591  islinds2  22013  lindsind2  22019  restcld  23379  ufprim  24117  volun  25755  itgsplitioo  26048  uhgr0vb  29477  uhgr0  29478  uvtxupgrres  29816  cplgr3v  29843  ex-dif  30845  indifundif  32941  imadifxp  33017  aciunf1  33079  indsupp  33257  pmtrcnelor  33475  lindsunlem  34078  lindsun  34079  braew  34697  carsgclctunlem1  34772  carsggect  34773  coinflippvt  34940  ballotlemfval0  34951  signstfvcl  35025  satf0  35901  onint1  37017  bj-2upln1upl  37717  bj-disj2r  37721  lindsenlbs  38323  poimirlem13  38341  poimirlem14  38342  poimirlem18  38346  poimirlem21  38349  poimirlem30  38358  itg2addnclem  38379  asindmre  38411  disjresundif  38953  dmxrnuncnvepres  39099  dmxrncnvepres2  39140  sucdifsn  39193  ressucdifsn  39195  kelac2  43850  fourierdlem102  46980  fourierdlem114  46992  pwsal  47087  issald  47105  sge0fodjrnlem  47188  hoiprodp1  47360  lincext2  49292  disjdifb  49645