Theorem difeq2i 4146

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 4143	. 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  dfun3  4295  dfin3  4296  dfin4  4297  invdif  4298  indif  4299  difundi  4309  difindi  4311  difdif2  4315  dif32  4321  difabs  4322  dfsymdif3  4325  notrab  4341  dif0  4400  unvdif  4498  difdifdir  4515  dfif3  4562  difpr  4828  iinvdif  5103  cnvin  6176  fndifnfp  7210  dif1o  8556  dfsdom2  9162  brttrcl2  9783  ttrcltr  9785  rnttrcl  9791  dju1dif  10242  m1bits  16486  clsval2  23079  mretopd  23121  cmpfi  23437  llycmpkgen2  23579  pserdvlem2  26490  nbgrssvwo2  29397  finsumvtxdg2ssteplem1  29581  frgrwopreglem3  30346  iundifdifd  32584  iundifdif  32585  difres  32622  gsumhashmul  33040  pmtrcnelor  33084  cycpmconjv  33135  cyc3conja  33150  sibfof  34305  eulerpartlemmf  34340  kur14lem2  35175  kur14lem6  35179  kur14lem7  35180  satfv1  35331  dfon4  35857  onint1  36415  bj-2upln1upl  36990  poimirlem8  37588  dfssr2  38455  prjspval2  42568  diophren  42769  ordeldif1o  43222  nonrel  43546  dssmapntrcls  44090  salincl  46245  meaiuninc  46402  carageniuncllem1  46442  iscnrm3rlem3  48622