Theorem difeq2i 4086

Description: Inference adding difference to the left in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
difeq2i	⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)

Proof of Theorem difeq2i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		difeq2 4083	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)

Syntax hints:   = wceq 1567   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-dif 3916

This theorem is referenced by:  difeq12i  4087  dfun3  4237  dfin3  4238  dfin4  4239  invdif  4240  indif  4241  difundi  4251  difindi  4253  difdif2  4257  dif32  4263  difabs  4264  dfsymdif3  4267  notrab  4283  dif0  4341  unvdif  4441  difdifdir  4457  dfif3  4507  difpr  4775  iinvdif  5050  cnvin  6142  fndifnfp  7175  dif1o  8484  dfsdom2  9087  brttrcl2  9682  ttrcltr  9684  rnttrcl  9690  dju1dif  10155  m1bits  16497  clsval2  23175  mretopd  23217  cmpfi  23533  llycmpkgen2  23675  pserdvlem2  26556  nbgrssvwo2  29652  finsumvtxdg2ssteplem1  29835  frgrwopreglem3  30605  iundifdifd  32846  iundifdif  32847  difres  32885  gsumhashmul  33327  pmtrcnelor  33351  cycpmconjv  33402  cyc3conja  33417  elrgspnsubrunlem2  33508  evlextv  33876  sibfof  34674  eulerpartlemmf  34709  fineqvnttrclselem1  35456  kur14lem2  35597  kur14lem6  35601  kur14lem7  35602  satfv1  35753  dfon4  36281  onint1  36848  bj-2upln1upl  37547  poimirlem8  38166  dmcnvep  38926  dfssr2  39117  prjspval2  43236  diophren  43431  ordeldif1o  43878  nonrel  44201  dssmapntrcls  44745  salincl  46929  meaiuninc  47086  carageniuncllem1  47126  iscnrm3rlem3  49604