Theorem difeq1i 3757

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

Syntax hints:   = wceq 1523   ∖ cdif 3604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-dif 3610

This theorem is referenced by:  difeq12i  3759  dfin3  3899  indif1  3904  indifcom  3905  difun1  3920  notab  3930  notrab  3937  undifabs  4078  difprsn1  4362  difprsn2  4363  diftpsn3  4364  resdifcom  5450  resdmdfsn  5480  wfi  5751  orddif  5858  fresaun  6113  f12dfv  6569  f13dfv  6570  domunsncan  8101  phplem1  8180  elfiun  8377  axcclem  9317  dfn2  11343  mvdco  17911  pmtrdifellem2  17943  islinds2  20200  lindsind2  20206  restcld  21024  ufprim  21760  volun  23359  itgsplitioo  23649  uhgr0vb  26012  uhgr0  26013  uvtxupgrres  26359  cplgr3v  26387  ex-dif  27410  indifundif  29482  imadifxp  29540  aciunf1  29591  braew  30433  carsgclctunlem1  30507  carsggect  30508  coinflippvt  30674  ballotlemfval0  30685  signstfvcl  30778  frpoind  31865  frind  31868  onint1  32573  bj-2upln1upl  33137  bj-disj2r  33138  lindsenlbs  33534  poimirlem13  33552  poimirlem14  33553  poimirlem18  33557  poimirlem21  33560  poimirlem30  33569  itg2addnclem  33591  asindmre  33625  kelac2  37952  fourierdlem102  40743  fourierdlem114  40755  pwsal  40853  issald  40869  sge0fodjrnlem  40951  hoiprodp1  41123  lincext2  42569