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

Theorem abssi 3575
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 3572 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2607 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3536 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   {cab 2452    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490
This theorem is referenced by:  ssab2  3584  abf  3819  intab  4312  opabss  4508  relopabi  5128  exse2  6723  opiota  6843  tfrlem8  7053  fiprc  7597  fival  7872  hartogslem1  7967  tz9.12lem1  8205  rankuni  8281  scott0  8304  r0weon  8390  alephval3  8491  aceq3lem  8501  dfac5lem4  8507  dfac2  8511  cff  8628  cfsuc  8637  cff1  8638  cflim2  8643  cfss  8645  axdc3lem  8830  axdclem  8899  gruina  9196  nqpr  9392  infcvgaux1i  13631  4sqlem1  14325  sscpwex  15045  symgval  16209  cssval  18508  hauspwpwf1  20251  itg2lcl  21897  2sqlem7  23401  nmcexi  26649  cnre2csqima  27557  colinearex  29315  itg2addnclem  29671  itg2addnc  29674  areacirc  29717  islocfin  29796  eldiophb  30322
  Copyright terms: Public domain W3C validator