Theorem difeq2i 4070

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

Syntax hints:   = wceq 1541   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-dif 3900

This theorem is referenced by:  difeq12i  4071  dfun3  4223  dfin3  4224  dfin4  4225  invdif  4226  indif  4227  difundi  4237  difindi  4239  difdif2  4243  dif32  4249  difabs  4250  dfsymdif3  4253  notrab  4269  dif0  4325  unvdif  4422  difdifdir  4439  dfif3  4487  difpr  4752  iinvdif  5026  cnvin  6091  fndifnfp  7110  dif1o  8415  dfsdom2  9013  brttrcl2  9604  ttrcltr  9606  rnttrcl  9612  dju1dif  10064  m1bits  16351  clsval2  22965  mretopd  23007  cmpfi  23323  llycmpkgen2  23465  pserdvlem2  26365  nbgrssvwo2  29340  finsumvtxdg2ssteplem1  29524  frgrwopreglem3  30294  iundifdifd  32541  iundifdif  32542  difres  32580  gsumhashmul  33041  pmtrcnelor  33060  cycpmconjv  33111  cyc3conja  33126  elrgspnsubrunlem2  33215  sibfof  34353  eulerpartlemmf  34388  fineqvnttrclselem1  35141  kur14lem2  35251  kur14lem6  35255  kur14lem7  35256  satfv1  35407  dfon4  35935  onint1  36491  bj-2upln1upl  37066  poimirlem8  37676  dmcnvep  38415  dfssr2  38544  prjspval2  42654  diophren  42854  ordeldif1o  43301  nonrel  43625  dssmapntrcls  44169  salincl  46370  meaiuninc  46527  carageniuncllem1  46567  iscnrm3rlem3  48981