Theorem difeq2i 4071

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-dif 3902

This theorem is used by:  difeq12i  4072  dfun3  4222  dfin3  4223  dfin4  4224  invdif  4225  indif  4226  difundi  4236  difindi  4238  difdif2  4242  dif32  4248  difabs  4249  dfsymdif3  4252  notrab  4268  dif0  4327  unvdif  4429  difdifdir  4447  dfif3  4497  difpr  4766  iinvdif  5040  cnvin  6135  fndifnfp  7179  dif1o  8501  dfsdom2  9112  brttrcl2  9708  ttrcltr  9710  rnttrcl  9716  dju1dif  10244  m1bits  16603  clsval2  23361  mretopd  23403  cmpfi  23719  llycmpkgen2  23862  pserdvlem2  26748  nbgrssvwo2  29936  finsumvtxdg2ssteplem1  30119  frgrwopreglem3  30908  iundifdifd  33149  iundifdif  33150  difres  33187  gsumhashmul  33621  pmtrcnelor  33645  cycpmconjv  33696  cyc3conja  33711  elrgspnsubrunlem2  33802  evlextv  34167  sibfof  34965  eulerpartlemmf  35000  fineqvnttrclselem1  35772  kur14lem2  35951  kur14lem6  35955  kur14lem7  35956  satfv1  36107  dfon4  36635  onint1  37217  bj-2upln1upl  37917  poimirlem8  38526  dmcnvep  39300  dfssr2  39491  prjspval2  43621  diophren  43799  ordeldif1o  44246  nonrel  44569  dssmapntrcls  45113  salincl  47303  meaiuninc  47460  carageniuncllem1  47500  iscnrm3rlem3  50019