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

Theorem abssi 3516
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 3513 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2584 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3476 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   {cab 2448    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-in 3423  df-ss 3430
This theorem is referenced by:  ssab2  3525  abf  3780  intab  4279  opabss  4478  relopabi  4978  exse2  6759  opiota  6879  tfrlem8  7128  fiprc  7677  fival  7952  hartogslem1  8083  tz9.12lem1  8284  rankuni  8360  scott0  8383  r0weon  8469  alephval3  8567  aceq3lem  8577  dfac5lem4  8583  dfac2  8587  cff  8704  cfsuc  8713  cff1  8714  cflim2  8719  cfss  8721  axdc3lem  8906  axdclem  8975  gruina  9269  nqpr  9465  infcvgaux1i  13964  4sqlem1  14941  sscpwex  15769  symgval  17069  cssval  19294  islocfin  20581  hauspwpwf1  21051  itg2lcl  22734  2sqlem7  24347  isismt  24628  nmcexi  27728  dispcmp  28735  cnre2csqima  28766  mppspstlem  30258  colinearex  30876  itg2addnclem  32038  itg2addnc  32041  areacirc  32082  eldiophb  35644
  Copyright terms: Public domain W3C validator