Theorem difeq2i 4086

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

Syntax hints:   = wceq 1540   ∖ cdif 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-dif 3917

This theorem is referenced by:  difeq12i  4087  dfun3  4239  dfin3  4240  dfin4  4241  invdif  4242  indif  4243  difundi  4253  difindi  4255  difdif2  4259  dif32  4265  difabs  4266  dfsymdif3  4269  notrab  4285  dif0  4341  unvdif  4438  difdifdir  4455  dfif3  4503  difpr  4767  iinvdif  5044  cnvin  6117  fndifnfp  7150  dif1o  8464  dfsdom2  9064  brttrcl2  9667  ttrcltr  9669  rnttrcl  9675  dju1dif  10126  m1bits  16410  clsval2  22937  mretopd  22979  cmpfi  23295  llycmpkgen2  23437  pserdvlem2  26338  nbgrssvwo2  29289  finsumvtxdg2ssteplem1  29473  frgrwopreglem3  30243  iundifdifd  32490  iundifdif  32491  difres  32529  gsumhashmul  33001  pmtrcnelor  33048  cycpmconjv  33099  cyc3conja  33114  elrgspnsubrunlem2  33199  sibfof  34331  eulerpartlemmf  34366  kur14lem2  35194  kur14lem6  35198  kur14lem7  35199  satfv1  35350  dfon4  35881  onint1  36437  bj-2upln1upl  37012  poimirlem8  37622  dmcnvep  38361  dfssr2  38490  prjspval2  42601  diophren  42801  ordeldif1o  43249  nonrel  43573  dssmapntrcls  44117  salincl  46322  meaiuninc  46479  carageniuncllem1  46519  iscnrm3rlem3  48930