Theorem difeq2i 4098

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

Syntax hints:   = wceq 1540   ∖ cdif 3923

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-dif 3929

This theorem is referenced by:  difeq12i  4099  dfun3  4251  dfin3  4252  dfin4  4253  invdif  4254  indif  4255  difundi  4265  difindi  4267  difdif2  4271  dif32  4277  difabs  4278  dfsymdif3  4281  notrab  4297  dif0  4353  unvdif  4450  difdifdir  4467  dfif3  4515  difpr  4779  iinvdif  5056  cnvin  6133  fndifnfp  7168  dif1o  8512  dfsdom2  9110  brttrcl2  9728  ttrcltr  9730  rnttrcl  9736  dju1dif  10187  m1bits  16459  clsval2  22988  mretopd  23030  cmpfi  23346  llycmpkgen2  23488  pserdvlem2  26390  nbgrssvwo2  29341  finsumvtxdg2ssteplem1  29525  frgrwopreglem3  30295  iundifdifd  32542  iundifdif  32543  difres  32581  gsumhashmul  33055  pmtrcnelor  33102  cycpmconjv  33153  cyc3conja  33168  elrgspnsubrunlem2  33243  sibfof  34372  eulerpartlemmf  34407  kur14lem2  35229  kur14lem6  35233  kur14lem7  35234  satfv1  35385  dfon4  35911  onint1  36467  bj-2upln1upl  37042  poimirlem8  37652  dfssr2  38517  prjspval2  42636  diophren  42836  ordeldif1o  43284  nonrel  43608  dssmapntrcls  44152  salincl  46353  meaiuninc  46510  carageniuncllem1  46550  iscnrm3rlem3  48916