Theorem difeq2i 4054

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

Syntax hints:   = wceq 1539   ∖ cdif 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-dif 3890

This theorem is referenced by:  difeq12i  4055  dfun3  4199  dfin3  4200  dfin4  4201  invdif  4202  indif  4203  difundi  4213  difindi  4215  difdif2  4220  dif32  4226  difabs  4227  dfsymdif3  4230  notrab  4245  dif0  4306  unvdif  4408  difdifdir  4422  dfif3  4473  difpr  4736  iinvdif  5009  cnvin  6048  fndifnfp  7048  dif1o  8330  dfsdom2  8883  brttrcl2  9472  ttrcltr  9474  rnttrcl  9480  dju1dif  9928  m1bits  16147  clsval2  22201  mretopd  22243  cmpfi  22559  llycmpkgen2  22701  pserdvlem2  25587  nbgrssvwo2  27729  finsumvtxdg2ssteplem1  27912  frgrwopreglem3  28678  iundifdifd  30901  iundifdif  30902  difres  30939  gsumhashmul  31316  pmtrcnelor  31360  cycpmconjv  31409  cyc3conja  31424  sibfof  32307  eulerpartlemmf  32342  kur14lem2  33169  kur14lem6  33173  kur14lem7  33174  satfv1  33325  dfon4  34195  onint1  34638  bj-2upln1upl  35214  poimirlem8  35785  dfssr2  36617  prjspval2  40452  diophren  40635  nonrel  41192  dssmapntrcls  41738  salincl  43864  meaiuninc  44019  carageniuncllem1  44059  iscnrm3rlem3  46236