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 ⊢ (𝐶 ∖ 𝐴) = (𝐶 ∖ 𝐵)

Syntax hints:   = wceq 1542   ∖ cdif 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-dif 3892

This theorem is referenced by:  difeq12i  4064  dfun3  4216  dfin3  4217  dfin4  4218  invdif  4219  indif  4220  difundi  4230  difindi  4232  difdif2  4236  dif32  4242  difabs  4243  dfsymdif3  4246  notrab  4262  dif0  4318  unvdif  4415  difdifdir  4431  dfif3  4481  difpr  4748  iinvdif  5022  cnvin  6108  fndifnfp  7131  dif1o  8435  dfsdom2  9038  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  dju1dif  10095  m1bits  16409  clsval2  23015  mretopd  23057  cmpfi  23373  llycmpkgen2  23515  pserdvlem2  26393  nbgrssvwo2  29431  finsumvtxdg2ssteplem1  29614  frgrwopreglem3  30384  iundifdifd  32631  iundifdif  32632  difres  32670  gsumhashmul  33128  pmtrcnelor  33152  cycpmconjv  33203  cyc3conja  33218  elrgspnsubrunlem2  33309  evlextv  33686  sibfof  34484  eulerpartlemmf  34519  fineqvnttrclselem1  35265  kur14lem2  35389  kur14lem6  35393  kur14lem7  35394  satfv1  35545  dfon4  36073  onint1  36631  bj-2upln1upl  37331  poimirlem8  37949  dmcnvep  38709  dfssr2  38900  prjspval2  43046  diophren  43241  ordeldif1o  43688  nonrel  44011  dssmapntrcls  44555  salincl  46752  meaiuninc  46909  carageniuncllem1  46949  iscnrm3rlem3  49417