Theorem difeq2i 3988

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

Syntax hints:   = wceq 1508   ∖ cdif 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-ral 3095  df-rab 3099  df-dif 3834

This theorem is referenced by:  difeq12i  3989  dfun3  4132  dfin3  4133  dfin4  4134  invdif  4135  indif  4136  difundi  4146  difindi  4148  difdif2  4151  dif32  4157  difabs  4158  dfsymdif3  4159  notrab  4170  dif0  4221  unvdif  4309  difdifdir  4323  dfif3  4367  difpr  4615  iinvdif  4873  cnvin  5848  fndifnfp  6767  dif1o  7933  dfsdom2  8442  dju1dif  9402  m1bits  15655  clsval2  21377  mretopd  21419  cmpfi  21735  llycmpkgen2  21877  pserdvlem2  24734  nbgrssvwo2  26862  finsumvtxdg2ssteplem1  27045  frgrwopreglem3  27863  iundifdifd  30099  iundifdif  30100  difres  30133  sibfof  31275  eulerpartlemmf  31310  kur14lem2  32079  kur14lem6  32083  kur14lem7  32084  dfon4  32915  onint1  33357  bj-2upln1upl  33894  poimirlem8  34381  dfssr2  35224  prjspval2  38711  diophren  38847  nonrel  39347  dssmapntrcls  39882  salincl  42074  meaiuninc  42229  carageniuncllem1  42269