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

Theorem ss2abi 3565
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 3561 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1600 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   {cab 2445    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-in 3476  df-ss 3483
This theorem is referenced by:  abssi  3568  rabssab  3580  intabs  4601  abssexg  4625  imassrn  5339  fvclss  6133  fabexg  6730  f1oabexg  6733  mapex  7416  tc2  8162  hta  8304  infmap2  8587  cflm  8619  cflim2  8632  hsmex3  8803  domtriomlem  8811  axdc3lem2  8820  brdom7disj  8898  brdom6disj  8899  npex  9353  hashf1lem2  12458  issubc  15054  isghm  16055  symgbasfi  16199  tgval  19216  ustfn  20432  ustval  20433  ustn0  20451  birthdaylem1  23002  wlks  24181  trls  24200  mptctf  27202  measbase  27794  measval  27795  ismeas  27796  isrnmeas  27797  ballotlem2  28053  subfaclefac  28246  dfon2lem2  28779  sdclem2  29825  eldiophb  30281  hbtlem1  30665  hbtlem7  30667  rabexgf  30932  relopabVD  32656  lineset  34409  lautset  34753  pautsetN  34769  tendoset  35430
  Copyright terms: Public domain W3C validator