Theorem difeq1i 4070

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 3902

This theorem is used by:  difeq12i  4072  dfin3  4223  indif1  4228  indifcom  4229  difun1  4245  notab  4260  rabdif  4267  notrab  4268  undifabs  4434  difprsn1  4763  difprsn2  4764  diftpsn3  4765  resdifcom  5991  resdmdfsn  6025  resdmdfsnOLD  6026  frpoind  6340  orddif  6456  fresaun  6746  f12dfv  7274  f13dfv  7275  domunsncan  9075  elfiun  9400  frind  9732  dju1dif  10175  axcclem  10459  dfn2  12541  nulchn  18707  s1chn  18708  chnccat  18714  ex-chn1  18725  ex-chn2  18726  mvdco  19572  pmtrdifellem2  19604  islinds2  22026  lindsind2  22032  lindsenlbs  22064  restcld  23397  ufprim  24135  volun  25773  itgsplitioo  26065  uhgr0vb  29529  uhgr0  29530  uvtxupgrres  29868  cplgr3v  29895  ex-dif  30903  indifundif  32999  imadifxp  33074  aciunf1  33136  indsupp  33313  pmtrcnelor  33531  lindsunlem  34134  lindsun  34135  braew  34753  carsgclctunlem1  34828  carsggect  34829  coinflippvt  34996  ballotlemfval0  35007  signstfvcl  35081  satf0  35951  onint1  37068  bj-2upln1upl  37768  bj-disj2r  37772  poimirlem13  38382  poimirlem14  38383  poimirlem18  38387  poimirlem21  38390  poimirlem30  38399  itg2addnclem  38420  asindmre  38452  disjresundif  38994  dmxrnuncnvepres  39140  dmxrncnvepres2  39181  sucdifsn  39234  ressucdifsn  39236  kelac2  43906  fourierdlem102  47036  fourierdlem114  47048  pwsal  47143  issald  47161  sge0fodjrnlem  47244  hoiprodp1  47416  lincext2  49385  disjdifb  49738