Theorem difeq2i 4071

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 3902

This theorem is used by:  difeq12i  4072  dfun3  4222  dfin3  4223  dfin4  4224  invdif  4225  indif  4226  difundi  4236  difindi  4238  difdif2  4242  dif32  4248  difabs  4249  dfsymdif3  4252  notrab  4268  dif0  4327  unvdif  4429  difdifdir  4447  dfif3  4497  difpr  4766  iinvdif  5040  cnvin  6135  fndifnfp  7174  dif1o  8487  dfsdom2  9098  brttrcl2  9693  ttrcltr  9695  rnttrcl  9701  dju1dif  10175  m1bits  16530  clsval2  23275  mretopd  23317  cmpfi  23633  llycmpkgen2  23776  pserdvlem2  26664  nbgrssvwo2  29822  finsumvtxdg2ssteplem1  30005  frgrwopreglem3  30794  iundifdifd  33035  iundifdif  33036  difres  33073  gsumhashmul  33507  pmtrcnelor  33531  cycpmconjv  33582  cyc3conja  33597  elrgspnsubrunlem2  33688  evlextv  34052  sibfof  34851  eulerpartlemmf  34886  fineqvnttrclselem1  35647  kur14lem2  35786  kur14lem6  35790  kur14lem7  35791  satfv1  35942  dfon4  36470  onint1  37068  bj-2upln1upl  37768  poimirlem8  38377  dmcnvep  39136  dfssr2  39327  prjspval2  43459  diophren  43654  ordeldif1o  44101  nonrel  44424  dssmapntrcls  44968  salincl  47152  meaiuninc  47309  carageniuncllem1  47349  iscnrm3rlem3  49868