Theorem difeq2i 4123

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

Syntax hints:   = wceq 1540   ∖ cdif 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-dif 3954

This theorem is referenced by:  difeq12i  4124  dfun3  4276  dfin3  4277  dfin4  4278  invdif  4279  indif  4280  difundi  4290  difindi  4292  difdif2  4296  dif32  4302  difabs  4303  dfsymdif3  4306  notrab  4322  dif0  4378  unvdif  4475  difdifdir  4492  dfif3  4540  difpr  4803  iinvdif  5080  cnvin  6164  fndifnfp  7196  dif1o  8538  dfsdom2  9136  brttrcl2  9754  ttrcltr  9756  rnttrcl  9762  dju1dif  10213  m1bits  16477  clsval2  23058  mretopd  23100  cmpfi  23416  llycmpkgen2  23558  pserdvlem2  26472  nbgrssvwo2  29379  finsumvtxdg2ssteplem1  29563  frgrwopreglem3  30333  iundifdifd  32574  iundifdif  32575  difres  32613  gsumhashmul  33064  pmtrcnelor  33111  cycpmconjv  33162  cyc3conja  33177  elrgspnsubrunlem2  33252  sibfof  34342  eulerpartlemmf  34377  kur14lem2  35212  kur14lem6  35216  kur14lem7  35217  satfv1  35368  dfon4  35894  onint1  36450  bj-2upln1upl  37025  poimirlem8  37635  dfssr2  38500  prjspval2  42623  diophren  42824  ordeldif1o  43273  nonrel  43597  dssmapntrcls  44141  salincl  46339  meaiuninc  46496  carageniuncllem1  46536  iscnrm3rlem3  48839