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

Theorem abssi 3542
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 3539 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2569 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3502 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   {cab 2414    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-in 3449  df-ss 3456
This theorem is referenced by:  ssab2  3551  abf  3802  intab  4289  opabss  4487  relopabi  4979  exse2  6746  opiota  6866  tfrlem8  7110  fiprc  7658  fival  7932  hartogslem1  8057  tz9.12lem1  8257  rankuni  8333  scott0  8356  r0weon  8442  alephval3  8539  aceq3lem  8549  dfac5lem4  8555  dfac2  8559  cff  8676  cfsuc  8685  cff1  8686  cflim2  8691  cfss  8693  axdc3lem  8878  axdclem  8947  gruina  9242  nqpr  9438  infcvgaux1i  13893  4sqlem1  14855  sscpwex  15671  symgval  16971  cssval  19176  islocfin  20463  hauspwpwf1  20933  itg2lcl  22562  2sqlem7  24161  isismt  24439  nmcexi  27514  dispcmp  28525  cnre2csqima  28556  mppspstlem  29997  colinearex  30612  itg2addnclem  31697  itg2addnc  31700  areacirc  31741  eldiophb  35308
  Copyright terms: Public domain W3C validator