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

Theorem abssi 3248
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 3245 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2400 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3210 1  |-  { x  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   {cab 2269    C_ wss 3152
This theorem is referenced by:  ssab2  3257  abf  3488  intab  3892  opabss  4080  relopabi  4811  exse2  5047  opiota  6290  tfrlem8  6400  fiprc  6942  fival  7166  hartogslem1  7257  tz9.12lem1  7459  rankuni  7535  scott0  7556  r0weon  7640  alephval3  7737  aceq3lem  7747  dfac5lem4  7753  dfac2  7757  cff  7874  cfsuc  7883  cff1  7884  cflim2  7889  cfss  7891  axdc3lem  8076  axdclem  8146  gruina  8440  nqpr  8638  infcvgaux1i  12315  4sqlem1  12995  sscpwex  13692  symgval  14771  cssval  16582  hauspwpwf1  17682  itg2lcl  19082  2sqlem7  20609  nmcexi  22606  cnre2csqima  23295  colinearex  24683  areacirc  24931  stcat  25044  prodex  25304  cntrset  25602  islocfin  26296  eldiophb  26836
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator