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

Theorem abssi 3415
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 3412 . 2  |-  { x  |  ph }  C_  { x  |  x  e.  A }
3 abid2 2550 . 2  |-  { x  |  x  e.  A }  =  A
42, 3sseqtri 3376 1  |-  { x  |  ph }  C_  A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   {cab 2419    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-in 3323  df-ss 3330
This theorem is referenced by:  ssab2  3424  abf  3659  intab  4146  opabss  4341  relopabi  4952  exse2  6506  opiota  6622  tfrlem8  6829  fiprc  7379  fival  7650  hartogslem1  7744  tz9.12lem1  7982  rankuni  8058  scott0  8081  r0weon  8167  alephval3  8268  aceq3lem  8278  dfac5lem4  8284  dfac2  8288  cff  8405  cfsuc  8414  cff1  8415  cflim2  8420  cfss  8422  axdc3lem  8607  axdclem  8676  gruina  8973  nqpr  9171  infcvgaux1i  13302  4sqlem1  13992  sscpwex  14711  symgval  15864  cssval  17949  hauspwpwf1  19402  itg2lcl  21047  2sqlem7  22594  nmcexi  25253  cnre2csqima  26195  colinearex  27938  itg2addnclem  28287  itg2addnc  28290  areacirc  28333  islocfin  28412  eldiophb  28940
  Copyright terms: Public domain W3C validator