Theorem difeq2i 3758

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

Syntax hints:   = wceq 1523   ∖ cdif 3604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-rab 2950  df-dif 3610

This theorem is referenced by:  difeq12i  3759  dfun3  3898  dfin3  3899  dfin4  3900  invdif  3901  indif  3902  difundi  3912  difindi  3914  difdif2  3917  dif32  3924  difabs  3925  dfsymdif3  3926  notrab  3937  dif0  3983  unvdif  4075  difdifdir  4089  dfif3  4133  difpr  4366  iinvdif  4624  cnvin  5575  fndifnfp  6483  dif1o  7625  dfsdom2  8124  cda1dif  9036  m1bits  15209  clsval2  20902  mretopd  20944  cmpfi  21259  llycmpkgen2  21401  pserdvlem2  24227  nbgrssvwo2  26303  nbgrssvwo2OLD  26306  finsumvtxdg2ssteplem1  26497  clwwlknclwwlkdifsOLD  26947  frgrwopreglem3  27294  iundifdifd  29506  iundifdif  29507  difres  29539  sibfof  30530  eulerpartlemmf  30565  kur14lem2  31315  kur14lem6  31319  kur14lem7  31320  dfon4  32125  onint1  32573  bj-2upln1upl  33137  poimirlem8  33547  dfssr2  34389  diophren  37694  nonrel  38207  dssmapntrcls  38743  salincl  40861  meaiuninc  41016  carageniuncllem1  41056