Theorem difeq1i 3571

Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
difeq1i.1	|- A = B

Assertion

Ref	Expression
difeq1i	|- ( A \ C ) = ( B \ C )

Proof of Theorem difeq1i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 |- A = B
2		difeq1 3568	. 2 |- ( A = B -> ( A \ C ) = ( B \ C ) )
3	1, 2	ax-mp 5	1 |- ( A \ C ) = ( B \ C )

Syntax hints:   = wceq 1370   \ cdif 3426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-dif 3432

This theorem is referenced by:  difeq12i  3573  dfin3  3690  indif1  3695  indifcom  3696  difun1  3711  notab  3721  notrab  3728  undifabs  3857  difprsn1  4111  difprsn2  4112  orddif  4913  resdmdfsn  5253  fresaun  5683  domunsncan  7514  phplem1  7593  elfiun  7784  axcclem  8730  dfn2  10696  mvdco  16062  pmtrdifellem2  16094  islinds2  18360  lindsind2  18366  restcld  18901  bwthOLD  19139  ufprim  19607  volun  21152  itgsplitioo  21441  uhgra0v  23389  usgra0v  23435  usgra1v  23453  cusgra3v  23517  ex-dif  23775  imadifxp  26083  braew  26795  coinflippvt  27004  ballotlemfval0  27015  signstfvcl  27111  wfi  27805  frind  27841  onint1  28432  itg2addnclem  28584  asindmre  28620  kelac2  29559  f12dfv  30287  f13dfv  30288  lincext2  31099  bj-2upln1upl  32820