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

Theorem ss2abi 3245
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 3241 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1537 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4   {cab 2269    C_ wss 3152
This theorem is referenced by:  abssi  3248  rabssab  3259  intabs  4172  abssexg  4195  imassrn  5025  fabexg  5422  f1oabexg  5484  fvclss  5760  mapex  6778  tc2  7427  hta  7567  infmap2  7844  cflm  7876  cflim2  7889  hsmex3  8060  domtriomlem  8068  axdc3lem2  8077  brdom7disj  8156  brdom6disj  8157  npex  8610  hashf1lem2  11394  issubc  13712  isghm  14683  tgval  16693  birthdaylem1  20246  ballotlem2  23047  mptctf  23348  measbase  23528  measval  23529  ismeas  23530  isrnmeas  23531  subfaclefac  23707  dfon2lem2  24140  elixp2b  25154  posprsr  25240  sdclem2  26452  eldiophb  26836  rencldnfilem  26903  uvcff  27240  hbtlem1  27327  hbtlem7  27329  rabexgf  27695  relopabVD  28677  lineset  29927  lautset  30271  pautsetN  30287  tendoset  30948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator