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

Theorem abssi 3574
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 3571 . 2
3 abid2 2597 . 2
42, 3sseqtri 3535 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  {cab 2442  C_wss 3475
This theorem is referenced by:  ssab2  3583  abf  3819  intab  4317  opabss  4513  relopabi  5133  exse2  6739  opiota  6859  tfrlem8  7072  fiprc  7617  fival  7892  hartogslem1  7988  tz9.12lem1  8226  rankuni  8302  scott0  8325  r0weon  8411  alephval3  8512  aceq3lem  8522  dfac5lem4  8528  dfac2  8532  cff  8649  cfsuc  8658  cff1  8659  cflim2  8664  cfss  8666  axdc3lem  8851  axdclem  8920  gruina  9217  nqpr  9413  infcvgaux1i  13668  4sqlem1  14466  sscpwex  15184  symgval  16404  cssval  18713  islocfin  20018  hauspwpwf1  20488  itg2lcl  22134  2sqlem7  23645  isismt  23921  nmcexi  26945  dispcmp  27862  cnre2csqima  27893  mppspstlem  28931  colinearex  29710  itg2addnclem  30066  itg2addnc  30069  areacirc  30112  eldiophb  30690
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-or 370  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-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator