Theorem difeq2i 4063

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-dif 4050

This theorem is used by:  difeq12i  4064  dfun3  4224  dfin3  4225  dfin4  4226  invdif  4227  indif  4228  difundi  4238  difindi  4240  difdif2  4244  dif32  4250  difabs  4251  dfsymdif3  4254  notrab  4270  dif0  4330  unvdif  4432  difdifdir  4450  dfif3  4500  difpr  4768  iinvdif  5045  cnvin  6153  fndifnfp  7212  dif1o  8546  dfsdom2  9157  brttrcl2  9752  ttrcltr  9754  rnttrcl  9760  dju1dif  10290  m1bits  16654  clsval2  23423  mretopd  23465  cmpfi  23781  llycmpkgen2  23924  pserdvlem2  26812  nbgrssvwo2  30000  finsumvtxdg2ssteplem1  30183  frgrwopreglem3  30972  iundifdifd  33254  iundifdif  33255  difres  33292  gsumhashmul  33727  pmtrcnelor  33751  cycpmconjv  33802  cyc3conja  33817  elrgspnsubrunlem2  33908  evlextv  34285  sibfof  35083  eulerpartlemmf  35118  fineqvnttrclselem1  35930  kur14lem2  36180  kur14lem6  36184  kur14lem7  36185  satfv1  36336  dfon4  36870  onint1  37452  bj-2upln1upl  38152  poimirlem8  38814  dmcnvep  39586  dfssr2  39777  prjspval2  43907  diophren  44086  ordeldif1o  44523  nonrel  44846  dssmapntrcls  45389  salincl  47607  meaiuninc  47764  carageniuncllem1  47804  iscnrm3rlem3  50387