Theorem difeq1i 4067

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

Syntax hints:   = wceq 1541   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-dif 3900

This theorem is referenced by:  difeq12i  4069  dfin3  4222  indif1  4227  indifcom  4228  difun1  4244  notab  4259  rabdif  4266  notrab  4267  undifabs  4423  difprsn1  4747  difprsn2  4748  diftpsn3  4749  resdifcom  5942  resdmdfsn  5975  frpoind  6284  orddif  6399  fresaun  6689  f12dfv  7202  f13dfv  7203  domunsncan  8985  elfiun  9309  frind  9638  dju1dif  10059  axcclem  10343  dfn2  12389  nulchn  18520  s1chn  18521  chnccat  18527  ex-chn1  18538  ex-chn2  18539  mvdco  19352  pmtrdifellem2  19384  islinds2  21745  lindsind2  21751  restcld  23082  ufprim  23819  volun  25468  itgsplitioo  25761  uhgr0vb  29045  uhgr0  29046  uvtxupgrres  29381  cplgr3v  29408  ex-dif  30395  indifundif  32496  imadifxp  32573  aciunf1  32637  indsupp  32840  pmtrcnelor  33052  lindsunlem  33629  lindsun  33630  braew  34247  carsgclctunlem1  34322  carsggect  34323  coinflippvt  34490  ballotlemfval0  34501  signstfvcl  34578  satf0  35408  onint1  36483  bj-2upln1upl  37058  bj-disj2r  37062  lindsenlbs  37655  poimirlem13  37673  poimirlem14  37674  poimirlem18  37678  poimirlem21  37681  poimirlem30  37690  itg2addnclem  37711  asindmre  37743  sucdifsn  38273  disjresundif  38277  ressucdifsn  38279  kelac2  43098  fourierdlem102  46246  fourierdlem114  46258  pwsal  46353  issald  46371  sge0fodjrnlem  46454  hoiprodp1  46626  lincext2  48487  disjdifb  48841