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

Theorem ss2abi 3525
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 3521 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1596 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   {cab 2436    C_ wss 3429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-in 3436  df-ss 3443
This theorem is referenced by:  abssi  3528  rabssab  3540  intabs  4554  abssexg  4578  imassrn  5281  fvclss  6061  fabexg  6636  f1oabexg  6639  mapex  7323  tc2  8066  hta  8208  infmap2  8491  cflm  8523  cflim2  8536  hsmex3  8707  domtriomlem  8715  axdc3lem2  8724  brdom7disj  8802  brdom6disj  8803  npex  9259  hashf1lem2  12320  issubc  14859  isghm  15858  symgbasfi  16002  tgval  18685  ustfn  19901  ustval  19902  ustn0  19920  birthdaylem1  22471  wlks  23570  trls  23580  mptctf  26165  measbase  26749  measval  26750  ismeas  26751  isrnmeas  26752  ballotlem2  27008  subfaclefac  27201  dfon2lem2  27734  sdclem2  28779  eldiophb  29236  hbtlem1  29620  hbtlem7  29622  rabexgf  29887  relopabVD  31940  lineset  33691  lautset  34035  pautsetN  34051  tendoset  34712
  Copyright terms: Public domain W3C validator