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

Theorem ss2abi 3468
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 3464 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1676 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   {cab 2437    C_ wss 3371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-in 3378  df-ss 3385
This theorem is referenced by:  abssi  3471  rabssab  3483  intabs  4536  abssexg  4560  imassrn  5156  fvclss  6132  fabexg  6736  f1oabexg  6739  mapex  7464  tc2  8212  hta  8354  infmap2  8634  cflm  8666  cflim2  8679  hsmex3  8850  domtriomlem  8858  axdc3lem2  8867  brdom7disj  8945  brdom6disj  8946  npex  9397  hashf1lem2  12613  issubc  15750  isghm  16893  symgbasfi  17037  tgval  19980  ustfn  21226  ustval  21227  ustn0  21245  birthdaylem1  23888  wlks  25258  trls  25277  mptctf  28312  measbase  29025  measval  29026  ismeas  29027  isrnmeas  29028  ballotlem2  29326  subfaclefac  29904  dfon2lem2  30435  poimirlem4  31945  poimirlem9  31950  poimirlem26  31967  poimirlem27  31968  poimirlem28  31969  poimirlem32  31973  sdclem2  32072  lineset  33304  lautset  33648  pautsetN  33664  tendoset  34327  eldiophb  35600  hbtlem1  35983  hbtlem7  35985  relopabVD  37294  rabexgf  37341  rgrprc  39707  1wlksfval  39725  wlksfval  39726
  Copyright terms: Public domain W3C validator