Theorem difeq2i 4075

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

Syntax hints:   = wceq 1541   ∖ cdif 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904

This theorem is referenced by:  difeq12i  4076  dfun3  4228  dfin3  4229  dfin4  4230  invdif  4231  indif  4232  difundi  4242  difindi  4244  difdif2  4248  dif32  4254  difabs  4255  dfsymdif3  4258  notrab  4274  dif0  4330  unvdif  4427  difdifdir  4444  dfif3  4494  difpr  4759  iinvdif  5035  cnvin  6102  fndifnfp  7122  dif1o  8427  dfsdom2  9028  brttrcl2  9623  ttrcltr  9625  rnttrcl  9631  dju1dif  10083  m1bits  16367  clsval2  22994  mretopd  23036  cmpfi  23352  llycmpkgen2  23494  pserdvlem2  26394  nbgrssvwo2  29435  finsumvtxdg2ssteplem1  29619  frgrwopreglem3  30389  iundifdifd  32636  iundifdif  32637  difres  32675  gsumhashmul  33150  pmtrcnelor  33173  cycpmconjv  33224  cyc3conja  33239  elrgspnsubrunlem2  33330  evlextv  33707  sibfof  34497  eulerpartlemmf  34532  fineqvnttrclselem1  35277  kur14lem2  35401  kur14lem6  35405  kur14lem7  35406  satfv1  35557  dfon4  36085  onint1  36643  bj-2upln1upl  37225  poimirlem8  37829  dmcnvep  38573  dfssr2  38752  prjspval2  42856  diophren  43055  ordeldif1o  43502  nonrel  43825  dssmapntrcls  44369  salincl  46568  meaiuninc  46725  carageniuncllem1  46765  iscnrm3rlem3  49187