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

Theorem ss2abi 3258
Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)
Hypothesis
Ref Expression
ss2abi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ss2abi  |-  { x  |  ph }  C_  { x  |  ps }

Proof of Theorem ss2abi
StepHypRef Expression
1 ss2ab 3254 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1540 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4   {cab 2282    C_ wss 3165
This theorem is referenced by:  abssi  3261  rabssab  3272  intabs  4188  abssexg  4211  imassrn  5041  fabexg  5438  f1oabexg  5500  fvclss  5776  mapex  6794  tc2  7443  hta  7583  infmap2  7860  cflm  7892  cflim2  7905  hsmex3  8076  domtriomlem  8084  axdc3lem2  8093  brdom7disj  8172  brdom6disj  8173  npex  8626  hashf1lem2  11410  issubc  13728  isghm  14699  tgval  16709  birthdaylem1  20262  ballotlem2  23063  mptctf  23363  measbase  23543  measval  23544  ismeas  23545  isrnmeas  23546  subfaclefac  23722  dfon2lem2  24211  elixp2b  25257  posprsr  25343  sdclem2  26555  eldiophb  26939  rencldnfilem  27006  uvcff  27343  hbtlem1  27430  hbtlem7  27432  rabexgf  27798  wlks  28328  trls  28335  relopabVD  28993  lineset  30549  lautset  30893  pautsetN  30909  tendoset  31570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator