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

Theorem ss2abi 3415
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 3411 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1559 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4   {cab 2422    C_ wss 3320
This theorem is referenced by:  abssi  3418  rabssab  3430  intabs  4361  abssexg  4384  imassrn  5216  fabexg  5624  f1oabexg  5686  fvclss  5980  mapex  7024  tc2  7681  hta  7821  infmap2  8098  cflm  8130  cflim2  8143  hsmex3  8314  domtriomlem  8322  axdc3lem2  8331  brdom7disj  8409  brdom6disj  8410  npex  8863  hashf1lem2  11705  issubc  14035  isghm  15006  tgval  17020  ustfn  18231  ustval  18232  ustn0  18250  birthdaylem1  20790  wlks  21526  trls  21536  mptctf  24112  measbase  24551  measval  24552  ismeas  24553  isrnmeas  24554  ballotlem2  24746  subfaclefac  24862  dfon2lem2  25411  sdclem2  26446  eldiophb  26815  uvcff  27217  hbtlem1  27304  hbtlem7  27306  rabexgf  27671  relopabVD  29013  lineset  30535  lautset  30879  pautsetN  30895  tendoset  31556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator