Theorem difeq1i 4145

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

Syntax hints:   = wceq 1537   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-dif 3979

This theorem is referenced by:  difeq12i  4147  dfin3  4296  indif1  4301  indifcom  4302  difun1  4318  notab  4333  rabdif  4340  notrab  4341  undifabs  4501  difprsn1  4825  difprsn2  4826  diftpsn3  4827  resdifcom  6028  resdmdfsn  6060  frpoind  6374  wfiOLD  6383  orddif  6491  fresaun  6792  f12dfv  7309  f13dfv  7310  domunsncan  9138  phplem1OLD  9280  elfiun  9499  frind  9819  dju1dif  10242  axcclem  10526  dfn2  12566  mvdco  19487  pmtrdifellem2  19519  islinds2  21856  lindsind2  21862  restcld  23201  ufprim  23938  volun  25599  itgsplitioo  25893  uhgr0vb  29107  uhgr0  29108  uvtxupgrres  29443  cplgr3v  29470  ex-dif  30455  indifundif  32554  imadifxp  32623  aciunf1  32681  pmtrcnelor  33084  lindsunlem  33637  lindsun  33638  braew  34206  carsgclctunlem1  34282  carsggect  34283  coinflippvt  34449  ballotlemfval0  34460  signstfvcl  34550  satf0  35340  onint1  36415  bj-2upln1upl  36990  bj-disj2r  36994  lindsenlbs  37575  poimirlem13  37593  poimirlem14  37594  poimirlem18  37598  poimirlem21  37601  poimirlem30  37610  itg2addnclem  37631  asindmre  37663  sucdifsn  38194  disjresundif  38198  ressucdifsn  38200  kelac2  43022  fourierdlem102  46129  fourierdlem114  46141  pwsal  46236  issald  46254  sge0fodjrnlem  46337  hoiprodp1  46509  lincext2  48184  disjdifb  48541