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

Theorem abssi 3378
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 3375 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2521 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3340 1  |-  { x  |  ph }  C_  A
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   {cab 2390    C_ wss 3280
This theorem is referenced by:  ssab2  3387  abf  3621  intab  4040  opabss  4229  relopabi  4959  exse2  5197  opiota  6494  tfrlem8  6604  fiprc  7147  fival  7375  hartogslem1  7467  tz9.12lem1  7669  rankuni  7745  scott0  7766  r0weon  7850  alephval3  7947  aceq3lem  7957  dfac5lem4  7963  dfac2  7967  cff  8084  cfsuc  8093  cff1  8094  cflim2  8099  cfss  8101  axdc3lem  8286  axdclem  8355  gruina  8649  nqpr  8847  infcvgaux1i  12591  4sqlem1  13271  sscpwex  13970  symgval  15049  cssval  16864  hauspwpwf1  17972  itg2lcl  19572  2sqlem7  21107  nmcexi  23482  cnre2csqima  24262  colinearex  25898  itg2addnclem  26155  itg2addnc  26158  areacirc  26187  islocfin  26266  eldiophb  26705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator