Theorem difeq1i 4074

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

Syntax hints:   = wceq 1559   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3905

This theorem is referenced by:  difeq12i  4076  dfin3  4227  indif1  4232  indifcom  4233  difun1  4249  notab  4264  rabdif  4271  notrab  4272  undifabs  4429  difprsn1  4757  difprsn2  4758  diftpsn3  4759  resdifcom  5980  resdmdfsn  6014  resdmdfsnOLD  6015  frpoind  6324  orddif  6439  fresaun  6730  f12dfv  7252  f13dfv  7253  domunsncan  9043  elfiun  9370  frind  9702  dju1dif  10123  axcclem  10408  dfn2  12488  nulchn  18642  s1chn  18643  chnccat  18649  ex-chn1  18660  ex-chn2  18661  mvdco  19476  pmtrdifellem2  19508  islinds2  21853  lindsind2  21859  restcld  23220  ufprim  23957  volun  25595  itgsplitioo  25888  uhgr0vb  29230  uhgr0  29231  uvtxupgrres  29566  cplgr3v  29593  ex-dif  30582  indifundif  32683  imadifxp  32761  aciunf1  32826  indsupp  33006  pmtrcnelor  33232  lindsunlem  33882  lindsun  33883  braew  34500  carsgclctunlem1  34575  carsggect  34576  coinflippvt  34743  ballotlemfval0  34754  signstfvcl  34828  satf0  35683  onint1  36770  bj-2upln1upl  37470  bj-disj2r  37474  lindsenlbs  38075  poimirlem13  38093  poimirlem14  38094  poimirlem18  38098  poimirlem21  38101  poimirlem30  38110  itg2addnclem  38131  asindmre  38163  disjresundif  38706  dmxrnuncnvepres  38852  dmxrncnvepres2  38893  sucdifsn  38946  ressucdifsn  38948  kelac2  43603  fourierdlem102  46743  fourierdlem114  46755  pwsal  46850  issald  46868  sge0fodjrnlem  46951  hoiprodp1  47123  lincext2  49038  disjdifb  49392