Theorem difeq2i 4059

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

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-dif 4046

This theorem is used by:  difeq12i  4060  dfun3  4220  dfin3  4221  dfin4  4222  invdif  4223  indif  4224  difundi  4234  difindi  4236  difdif2  4240  dif32  4246  difabs  4247  dfsymdif3  4250  notrab  4266  dif0  4326  unvdif  4428  difdifdir  4446  dfif3  4496  difpr  4762  iinvdif  5039  cnvin  6137  fndifnfp  7185  dif1o  8515  dfsdom2  9126  brttrcl2  9722  ttrcltr  9724  rnttrcl  9730  dju1dif  10258  m1bits  16619  clsval2  23377  mretopd  23419  cmpfi  23735  llycmpkgen2  23878  pserdvlem2  26764  nbgrssvwo2  29952  finsumvtxdg2ssteplem1  30135  frgrwopreglem3  30924  iundifdifd  33207  iundifdif  33208  difres  33245  gsumhashmul  33678  pmtrcnelor  33702  cycpmconjv  33753  cyc3conja  33768  elrgspnsubrunlem2  33859  evlextv  34224  sibfof  35022  eulerpartlemmf  35057  fineqvnttrclselem1  35849  kur14lem2  36062  kur14lem6  36066  kur14lem7  36067  satfv1  36218  dfon4  36751  onint1  37333  bj-2upln1upl  38033  poimirlem8  38655  dmcnvep  39429  dfssr2  39620  prjspval2  43750  diophren  43929  ordeldif1o  44371  nonrel  44694  dssmapntrcls  45237  salincl  47442  meaiuninc  47599  carageniuncllem1  47639  iscnrm3rlem3  50164