Theorem difeq2i 3725

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

Syntax hints:   = wceq 1483   ∖ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-rab 2921  df-dif 3577

This theorem is referenced by:  difeq12i  3726  dfun3  3865  dfin3  3866  dfin4  3867  invdif  3868  indif  3869  difundi  3879  difindi  3881  difdif2  3884  dif32  3891  difabs  3892  dfsymdif3  3893  notrab  3904  dif0  3950  unvdif  4042  difdifdir  4056  dfif3  4100  difpr  4334  iinvdif  4592  cnvin  5540  fndifnfp  6442  dif1o  7580  dfsdom2  8083  cda1dif  8998  m1bits  15162  clsval2  20854  mretopd  20896  cmpfi  21211  llycmpkgen2  21353  pserdvlem2  24182  nbgrssvwo2  26261  finsumvtxdg2ssteplem1  26441  clwwlknclwwlkdifs  26873  frgrwopreglem3  27178  iundifdifd  29380  iundifdif  29381  difres  29413  sibfof  30402  eulerpartlemmf  30437  kur14lem2  31189  kur14lem6  31193  kur14lem7  31194  dfon4  32000  onint1  32448  bj-2upln1upl  33012  poimirlem8  33417  diophren  37377  nonrel  37890  dssmapntrcls  38426  salincl  40543  meaiuninc  40698  carageniuncllem1  40735