Theorem difeq2i 4047

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

Syntax hints:   = wceq 1538   ∖ cdif 3878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-dif 3884

This theorem is referenced by:  difeq12i  4048  dfun3  4192  dfin3  4193  dfin4  4194  invdif  4195  indif  4196  difundi  4206  difindi  4208  difdif2  4211  dif32  4217  difabs  4218  dfsymdif3  4221  notrab  4232  dif0  4286  unvdif  4381  difdifdir  4395  dfif3  4439  difpr  4696  iinvdif  4965  cnvin  5970  fndifnfp  6915  dif1o  8108  dfsdom2  8624  dju1dif  9583  m1bits  15779  clsval2  21655  mretopd  21697  cmpfi  22013  llycmpkgen2  22155  pserdvlem2  25023  nbgrssvwo2  27152  finsumvtxdg2ssteplem1  27335  frgrwopreglem3  28099  iundifdifd  30325  iundifdif  30326  difres  30363  gsumhashmul  30741  pmtrcnelor  30785  cycpmconjv  30834  cyc3conja  30849  sibfof  31708  eulerpartlemmf  31743  kur14lem2  32567  kur14lem6  32571  kur14lem7  32572  satfv1  32723  dfon4  33467  onint1  33910  bj-2upln1upl  34460  poimirlem8  35065  dfssr2  35899  prjspval2  39607  diophren  39754  nonrel  40284  dssmapntrcls  40831  salincl  42965  meaiuninc  43120  carageniuncllem1  43160