Theorem difeq1i 4122

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

Syntax hints:   = wceq 1540   ∖ cdif 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-dif 3954

This theorem is referenced by:  difeq12i  4124  dfin3  4277  indif1  4282  indifcom  4283  difun1  4299  notab  4314  rabdif  4321  notrab  4322  undifabs  4478  difprsn1  4800  difprsn2  4801  diftpsn3  4802  resdifcom  6016  resdmdfsn  6049  frpoind  6363  wfiOLD  6372  orddif  6480  fresaun  6779  f12dfv  7293  f13dfv  7294  domunsncan  9112  phplem1OLD  9254  elfiun  9470  frind  9790  dju1dif  10213  axcclem  10497  dfn2  12539  mvdco  19463  pmtrdifellem2  19495  islinds2  21833  lindsind2  21839  restcld  23180  ufprim  23917  volun  25580  itgsplitioo  25873  uhgr0vb  29089  uhgr0  29090  uvtxupgrres  29425  cplgr3v  29452  ex-dif  30442  indifundif  32543  imadifxp  32614  aciunf1  32673  indsupp  32852  s1chn  33000  pmtrcnelor  33111  lindsunlem  33675  lindsun  33676  braew  34243  carsgclctunlem1  34319  carsggect  34320  coinflippvt  34487  ballotlemfval0  34498  signstfvcl  34588  satf0  35377  onint1  36450  bj-2upln1upl  37025  bj-disj2r  37029  lindsenlbs  37622  poimirlem13  37640  poimirlem14  37641  poimirlem18  37645  poimirlem21  37648  poimirlem30  37657  itg2addnclem  37678  asindmre  37710  sucdifsn  38240  disjresundif  38244  ressucdifsn  38246  kelac2  43077  fourierdlem102  46223  fourierdlem114  46235  pwsal  46330  issald  46348  sge0fodjrnlem  46431  hoiprodp1  46603  lincext2  48372  disjdifb  48729