Theorem difeq1i 4076

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

Syntax hints:   = wceq 1542   ∖ cdif 3900

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-dif 3906

This theorem is referenced by:  difeq12i  4078  dfin3  4231  indif1  4236  indifcom  4237  difun1  4253  notab  4268  rabdif  4275  notrab  4276  undifabs  4432  difprsn1  4758  difprsn2  4759  diftpsn3  4760  resdifcom  5965  resdmdfsn  5998  frpoind  6308  orddif  6423  fresaun  6713  f12dfv  7229  f13dfv  7230  domunsncan  9017  elfiun  9345  frind  9674  dju1dif  10095  axcclem  10379  dfn2  12426  nulchn  18554  s1chn  18555  chnccat  18561  ex-chn1  18572  ex-chn2  18573  mvdco  19386  pmtrdifellem2  19418  islinds2  21780  lindsind2  21786  restcld  23128  ufprim  23865  volun  25514  itgsplitioo  25807  uhgr0vb  29157  uhgr0  29158  uvtxupgrres  29493  cplgr3v  29520  ex-dif  30510  indifundif  32611  imadifxp  32688  aciunf1  32753  indsupp  32960  pmtrcnelor  33185  lindsunlem  33802  lindsun  33803  braew  34420  carsgclctunlem1  34495  carsggect  34496  coinflippvt  34663  ballotlemfval0  34674  signstfvcl  34751  satf0  35588  onint1  36665  bj-2upln1upl  37272  bj-disj2r  37276  lindsenlbs  37866  poimirlem13  37884  poimirlem14  37885  poimirlem18  37889  poimirlem21  37892  poimirlem30  37901  itg2addnclem  37922  asindmre  37954  disjresundif  38497  dmxrnuncnvepres  38643  dmxrncnvepres2  38684  sucdifsn  38737  ressucdifsn  38739  kelac2  43422  fourierdlem102  46566  fourierdlem114  46578  pwsal  46673  issald  46691  sge0fodjrnlem  46774  hoiprodp1  46946  lincext2  48815  disjdifb  49169