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

Theorem abssi 3534
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 3531 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2594 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3495 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   {cab 2439    C_ wss 3435
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 3442  df-ss 3449
This theorem is referenced by:  ssab2  3543  abf  3778  intab  4265  opabss  4460  relopabi  5072  exse2  6626  opiota  6742  tfrlem8  6952  fiprc  7500  fival  7772  hartogslem1  7866  tz9.12lem1  8104  rankuni  8180  scott0  8203  r0weon  8289  alephval3  8390  aceq3lem  8400  dfac5lem4  8406  dfac2  8410  cff  8527  cfsuc  8536  cff1  8537  cflim2  8542  cfss  8544  axdc3lem  8729  axdclem  8798  gruina  9095  nqpr  9293  infcvgaux1i  13436  4sqlem1  14126  sscpwex  14846  symgval  16002  cssval  18231  hauspwpwf1  19691  itg2lcl  21337  2sqlem7  22841  nmcexi  25581  cnre2csqima  26485  colinearex  28234  itg2addnclem  28590  itg2addnc  28593  areacirc  28636  islocfin  28715  eldiophb  29242
  Copyright terms: Public domain W3C validator