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

Theorem ss2abi 3557
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 3553 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1609 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   {cab 2428    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475
This theorem is referenced by:  abssi  3560  rabssab  3572  intabs  4598  abssexg  4622  imassrn  5338  fvclss  6139  fabexg  6741  f1oabexg  6744  mapex  7428  tc2  8176  hta  8318  infmap2  8601  cflm  8633  cflim2  8646  hsmex3  8817  domtriomlem  8825  axdc3lem2  8834  brdom7disj  8912  brdom6disj  8913  npex  9367  hashf1lem2  12484  issubc  15081  isghm  16141  symgbasfi  16285  tgval  19329  ustfn  20577  ustval  20578  ustn0  20596  birthdaylem1  23153  wlks  24391  trls  24410  mptctf  27416  measbase  28041  measval  28042  ismeas  28043  isrnmeas  28044  ballotlem2  28300  subfaclefac  28493  dfon2lem2  29191  sdclem2  30210  eldiophb  30665  hbtlem1  31047  hbtlem7  31049  rabexgf  31353  relopabVD  33434  lineset  35202  lautset  35546  pautsetN  35562  tendoset  36225
  Copyright terms: Public domain W3C validator