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

Theorem abssi 3571
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 3568 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2597 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3531 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1819   {cab 2442    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3478  df-ss 3485
This theorem is referenced by:  ssab2  3580  abf  3828  intab  4319  opabss  4518  relopabi  5137  exse2  6738  opiota  6858  tfrlem8  7071  fiprc  7616  fival  7890  hartogslem1  7985  tz9.12lem1  8222  rankuni  8298  scott0  8321  r0weon  8407  alephval3  8508  aceq3lem  8518  dfac5lem4  8524  dfac2  8528  cff  8645  cfsuc  8654  cff1  8655  cflim2  8660  cfss  8662  axdc3lem  8847  axdclem  8916  gruina  9213  nqpr  9409  infcvgaux1i  13679  4sqlem1  14477  sscpwex  15230  symgval  16530  cssval  18839  islocfin  20143  hauspwpwf1  20613  itg2lcl  22259  2sqlem7  23770  isismt  24046  nmcexi  27071  dispcmp  28015  cnre2csqima  28046  mppspstlem  29106  colinearex  29872  itg2addnclem  30228  itg2addnc  30231  areacirc  30274  eldiophb  30852
  Copyright terms: Public domain W3C validator