Theorem difeq2i 4060

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

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

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 4047

This theorem is used by:  difeq12i  4061  dfun3  4221  dfin3  4222  dfin4  4223  invdif  4224  indif  4225  difundi  4235  difindi  4237  difdif2  4241  dif32  4247  difabs  4248  dfsymdif3  4251  notrab  4267  dif0  4326  unvdif  4428  difdifdir  4446  dfif3  4496  difpr  4765  iinvdif  5039  cnvin  6134  fndifnfp  7181  dif1o  8508  dfsdom2  9119  brttrcl2  9715  ttrcltr  9717  rnttrcl  9723  dju1dif  10251  m1bits  16610  clsval2  23368  mretopd  23410  cmpfi  23726  llycmpkgen2  23869  pserdvlem2  26755  nbgrssvwo2  29943  finsumvtxdg2ssteplem1  30126  frgrwopreglem3  30915  iundifdifd  33156  iundifdif  33157  difres  33194  gsumhashmul  33628  pmtrcnelor  33652  cycpmconjv  33703  cyc3conja  33718  elrgspnsubrunlem2  33809  evlextv  34174  sibfof  34972  eulerpartlemmf  35007  fineqvnttrclselem1  35789  kur14lem2  35972  kur14lem6  35976  kur14lem7  35977  satfv1  36128  dfon4  36655  onint1  37237  bj-2upln1upl  37937  poimirlem8  38547  dmcnvep  39321  dfssr2  39512  prjspval2  43642  diophren  43820  ordeldif1o  44262  nonrel  44585  dssmapntrcls  45128  salincl  47334  meaiuninc  47491  carageniuncllem1  47531  iscnrm3rlem3  50050