Theorem difeq1i 4088

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

Syntax hints:   = wceq 1540   ∖ cdif 3914

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920

This theorem is referenced by:  difeq12i  4090  dfin3  4243  indif1  4248  indifcom  4249  difun1  4265  notab  4280  rabdif  4287  notrab  4288  undifabs  4444  difprsn1  4767  difprsn2  4768  diftpsn3  4769  resdifcom  5972  resdmdfsn  6005  frpoind  6318  orddif  6433  fresaun  6734  f12dfv  7251  f13dfv  7252  domunsncan  9046  elfiun  9388  frind  9710  dju1dif  10133  axcclem  10417  dfn2  12462  mvdco  19382  pmtrdifellem2  19414  islinds2  21729  lindsind2  21735  restcld  23066  ufprim  23803  volun  25453  itgsplitioo  25746  uhgr0vb  29006  uhgr0  29007  uvtxupgrres  29342  cplgr3v  29369  ex-dif  30359  indifundif  32460  imadifxp  32537  aciunf1  32594  indsupp  32797  s1chn  32943  pmtrcnelor  33055  lindsunlem  33627  lindsun  33628  braew  34239  carsgclctunlem1  34315  carsggect  34316  coinflippvt  34483  ballotlemfval0  34494  signstfvcl  34571  satf0  35366  onint1  36444  bj-2upln1upl  37019  bj-disj2r  37023  lindsenlbs  37616  poimirlem13  37634  poimirlem14  37635  poimirlem18  37639  poimirlem21  37642  poimirlem30  37651  itg2addnclem  37672  asindmre  37704  sucdifsn  38234  disjresundif  38238  ressucdifsn  38240  kelac2  43061  fourierdlem102  46213  fourierdlem114  46225  pwsal  46320  issald  46338  sge0fodjrnlem  46421  hoiprodp1  46593  lincext2  48448  disjdifb  48802