Theorem difeq2i 4118

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

Syntax hints:   = wceq 1534   ∖ cdif 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-dif 3950

This theorem is referenced by:  difeq12i  4119  dfun3  4267  dfin3  4268  dfin4  4269  invdif  4270  indif  4271  difundi  4281  difindi  4283  difdif2  4288  dif32  4294  difabs  4295  dfsymdif3  4298  notrab  4314  dif0  4377  unvdif  4479  difdifdir  4496  dfif3  4547  difpr  4812  iinvdif  5088  cnvin  6156  fndifnfp  7190  dif1o  8530  dfsdom2  9134  brttrcl2  9757  ttrcltr  9759  rnttrcl  9765  dju1dif  10215  m1bits  16440  clsval2  23045  mretopd  23087  cmpfi  23403  llycmpkgen2  23545  pserdvlem2  26458  nbgrssvwo2  29298  finsumvtxdg2ssteplem1  29482  frgrwopreglem3  30247  iundifdifd  32482  iundifdif  32483  difres  32520  gsumhashmul  32925  pmtrcnelor  32969  cycpmconjv  33020  cyc3conja  33035  sibfof  34174  eulerpartlemmf  34209  kur14lem2  35035  kur14lem6  35039  kur14lem7  35040  satfv1  35191  dfon4  35717  onint1  36161  bj-2upln1upl  36731  poimirlem8  37329  dfssr2  38197  prjspval2  42267  diophren  42470  ordeldif1o  42926  nonrel  43251  dssmapntrcls  43795  salincl  45945  meaiuninc  46102  carageniuncllem1  46142  iscnrm3rlem3  48276