Theorem difeq1i 3724

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 3721	. 2 |- ( A = B -> ( A \ C ) = ( B \ C ) )
3	1, 2	ax-mp 5	1 |- ( A \ C ) = ( B \ C )

Syntax hints:   = wceq 1483   \ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-dif 3577

This theorem is referenced by:  difeq12i  3726  dfin3  3866  indif1  3871  indifcom  3872  difun1  3887  notab  3897  notrab  3904  undifabs  4045  difprsn1  4330  difprsn2  4331  diftpsn3  4332  resdifcom  5415  resdmdfsn  5445  wfi  5713  orddif  5820  fresaun  6075  f12dfv  6529  f13dfv  6530  domunsncan  8060  phplem1  8139  elfiun  8336  axcclem  9279  dfn2  11305  mvdco  17865  pmtrdifellem2  17897  islinds2  20152  lindsind2  20158  restcld  20976  ufprim  21713  volun  23313  itgsplitioo  23604  uhgr0vb  25967  uhgr0  25968  uvtxupgrres  26309  cplgr3v  26331  konigsbergiedgwOLD  27109  ex-dif  27280  indifundif  29356  imadifxp  29414  aciunf1  29463  braew  30305  carsgclctunlem1  30379  carsggect  30380  coinflippvt  30546  ballotlemfval0  30557  signstfvcl  30650  frind  31740  onint1  32448  bj-2upln1upl  33012  bj-disj2r  33013  lindsenlbs  33404  poimirlem13  33422  poimirlem14  33423  poimirlem18  33427  poimirlem21  33430  poimirlem30  33439  itg2addnclem  33461  asindmre  33495  kelac2  37635  fourierdlem102  40425  fourierdlem114  40437  pwsal  40535  issald  40551  sge0fodjrnlem  40633  hoiprodp1  40802  lincext2  42244