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

Theorem abssi 3404
Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
Hypothesis
Ref Expression
abssi.1
Assertion
Ref Expression
abssi
Distinct variable group:   ,

Proof of Theorem abssi
StepHypRef Expression
1 abssi.1 . . 3
21ss2abi 3401 . 2
3 abid2 2539 . 2
42, 3sseqtri 3365 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1749  {cab 2408  C_wss 3305
This theorem is referenced by:  ssab2  3413  abf  3648  intab  4133  opabss  4328  relopabi  4936  exse2  6487  opiota  6602  tfrlem8  6802  fiprc  7350  fival  7609  hartogslem1  7703  tz9.12lem1  7941  rankuni  8017  scott0  8040  r0weon  8126  alephval3  8227  aceq3lem  8237  dfac5lem4  8243  dfac2  8247  cff  8364  cfsuc  8373  cff1  8374  cflim2  8379  cfss  8381  axdc3lem  8566  axdclem  8635  gruina  8931  nqpr  9129  infcvgaux1i  13259  4sqlem1  13949  sscpwex  14668  symgval  15821  cssval  17815  hauspwpwf1  19264  itg2lcl  20905  2sqlem7  22450  nmcexi  25109  cnre2csqima  26050  colinearex  27793  itg2addnclem  28114  itg2addnc  28117  areacirc  28160  islocfin  28239  eldiophb  28768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-in 3312  df-ss 3319
  Copyright terms: Public domain W3C validator