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

Theorem abssi 3541
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 3538 . 2
3 abid2 2594 . 2
42, 3sseqtri 3502 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1758  {cab 2439  C_wss 3442
This theorem is referenced by:  ssab2  3550  abf  3785  intab  4275  opabss  4470  relopabi  5082  exse2  6650  opiota  6766  tfrlem8  6977  fiprc  7525  fival  7798  hartogslem1  7893  tz9.12lem1  8131  rankuni  8207  scott0  8230  r0weon  8316  alephval3  8417  aceq3lem  8427  dfac5lem4  8433  dfac2  8437  cff  8554  cfsuc  8563  cff1  8564  cflim2  8569  cfss  8571  axdc3lem  8756  axdclem  8825  gruina  9122  nqpr  9320  infcvgaux1i  13477  4sqlem1  14167  sscpwex  14887  symgval  16043  cssval  18300  hauspwpwf1  19959  itg2lcl  21605  2sqlem7  23109  nmcexi  25899  cnre2csqima  26798  colinearex  28547  itg2addnclem  28903  itg2addnc  28906  areacirc  28949  islocfin  29028  eldiophb  29555
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 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3449  df-ss 3456
  Copyright terms: Public domain W3C validator