Theorem difeq2i 4073

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

Syntax hints:   = wceq 1541   ∖ cdif 3896

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-dif 3902

This theorem is referenced by:  difeq12i  4074  dfun3  4226  dfin3  4227  dfin4  4228  invdif  4229  indif  4230  difundi  4240  difindi  4242  difdif2  4246  dif32  4252  difabs  4253  dfsymdif3  4256  notrab  4272  dif0  4328  unvdif  4425  difdifdir  4442  dfif3  4492  difpr  4757  iinvdif  5033  cnvin  6100  fndifnfp  7120  dif1o  8425  dfsdom2  9026  brttrcl2  9621  ttrcltr  9623  rnttrcl  9629  dju1dif  10081  m1bits  16365  clsval2  22992  mretopd  23034  cmpfi  23350  llycmpkgen2  23492  pserdvlem2  26392  nbgrssvwo2  29384  finsumvtxdg2ssteplem1  29568  frgrwopreglem3  30338  iundifdifd  32585  iundifdif  32586  difres  32624  gsumhashmul  33099  pmtrcnelor  33122  cycpmconjv  33173  cyc3conja  33188  elrgspnsubrunlem2  33279  evlextv  33656  sibfof  34446  eulerpartlemmf  34481  fineqvnttrclselem1  35226  kur14lem2  35350  kur14lem6  35354  kur14lem7  35355  satfv1  35506  dfon4  36034  onint1  36592  bj-2upln1upl  37168  poimirlem8  37768  dmcnvep  38512  dfssr2  38691  prjspval2  42798  diophren  42997  ordeldif1o  43444  nonrel  43767  dssmapntrcls  44311  salincl  46510  meaiuninc  46667  carageniuncllem1  46707  iscnrm3rlem3  49129