Theorem difeq2i 3918

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

Syntax hints:   = wceq 1637   ∖ cdif 3760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-ral 3097  df-rab 3101  df-dif 3766

This theorem is referenced by:  difeq12i  3919  dfun3  4061  dfin3  4062  dfin4  4063  invdif  4064  indif  4065  difundi  4075  difindi  4077  difdif2  4080  dif32  4086  difabs  4087  dfsymdif3  4088  notrab  4099  dif0  4145  unvdif  4232  difdifdir  4246  dfif3  4287  difpr  4518  iinvdif  4777  cnvin  5745  fndifnfp  6661  dif1o  7811  dfsdom2  8316  cda1dif  9277  m1bits  15375  clsval2  21062  mretopd  21104  cmpfi  21419  llycmpkgen2  21561  pserdvlem2  24390  nbgrssvwo2  26468  nbgrssvwo2OLD  26471  finsumvtxdg2ssteplem1  26663  clwwlknclwwlkdifsOLD  27116  frgrwopreglem3  27483  iundifdifd  29699  iundifdif  29700  difres  29732  sibfof  30721  eulerpartlemmf  30756  kur14lem2  31506  kur14lem6  31510  kur14lem7  31511  dfon4  32315  onint1  32759  bj-2upln1upl  33316  poimirlem8  33724  dfssr2  34556  diophren  37873  nonrel  38384  dssmapntrcls  38920  salincl  41016  meaiuninc  41171  carageniuncllem1  41211