MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difeq1i Unicode version

Theorem difeq1i 3617
Description: Inference adding difference to the right in a class equality. (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
difeq1i.1
Assertion
Ref Expression
difeq1i

Proof of Theorem difeq1i
StepHypRef Expression
1 difeq1i.1 . 2
2 difeq1 3614 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  \cdif 3472
This theorem is referenced by:  difeq12i  3619  dfin3  3736  indif1  3741  indifcom  3742  difun1  3757  notab  3767  notrab  3774  undifabs  3905  difprsn1  4166  difprsn2  4167  orddif  4976  resdmdfsn  5324  fresaun  5761  f12dfv  6179  f13dfv  6180  domunsncan  7637  phplem1  7716  elfiun  7910  axcclem  8858  dfn2  10833  mvdco  16470  pmtrdifellem2  16502  islinds2  18848  lindsind2  18854  restcld  19673  bwthOLD  19911  ufprim  20410  volun  21955  itgsplitioo  22244  uhgra0v  24310  usgra0v  24371  usgra1v  24390  cusgra3v  24464  ex-dif  25144  imadifxp  27458  braew  28214  coinflippvt  28423  ballotlemfval0  28434  signstfvcl  28530  wfi  29287  frind  29323  onint1  29914  itg2addnclem  30066  asindmre  30102  kelac2  31011  fourierdlem102  31991  fourierdlem114  32003  uhg0v  32377  uhgrepe  32378  lincext2  33056  bj-2upln1upl  34582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-dif 3478
  Copyright terms: Public domain W3C validator