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

Theorem abssi 3261
Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
Hypothesis
Ref Expression
abssi.1  |-  ( ph  ->  x  e.  A )
Assertion
Ref Expression
abssi  |-  { x  |  ph }  C_  A
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem abssi
StepHypRef Expression
1 abssi.1 . . 3  |-  ( ph  ->  x  e.  A )
21ss2abi 3258 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2413 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3223 1  |-  { x  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   {cab 2282    C_ wss 3165
This theorem is referenced by:  ssab2  3270  abf  3501  intab  3908  opabss  4096  relopabi  4827  exse2  5063  opiota  6306  tfrlem8  6416  fiprc  6958  fival  7182  hartogslem1  7273  tz9.12lem1  7475  rankuni  7551  scott0  7572  r0weon  7656  alephval3  7753  aceq3lem  7763  dfac5lem4  7769  dfac2  7773  cff  7890  cfsuc  7899  cff1  7900  cflim2  7905  cfss  7907  axdc3lem  8092  axdclem  8162  gruina  8456  nqpr  8654  infcvgaux1i  12331  4sqlem1  13011  sscpwex  13708  symgval  14787  cssval  16598  hauspwpwf1  17698  itg2lcl  19098  2sqlem7  20625  nmcexi  22622  cnre2csqima  23310  colinearex  24755  itg2addnclem  25003  itg2addnc  25005  areacirc  25034  stcat  25147  prodex  25407  cntrset  25705  islocfin  26399  eldiophb  26939
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator