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

Theorem ss2abi 3558
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 3554 . 2  |-  ( { x  |  ph }  C_ 
{ x  |  ps } 
<-> 
A. x ( ph  ->  ps ) )
2 ss2abi.1 . 2  |-  ( ph  ->  ps )
31, 2mpgbir 1627 1  |-  { x  |  ph }  C_  { x  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   {cab 2439    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3468  df-ss 3475
This theorem is referenced by:  abssi  3561  rabssab  3573  intabs  4598  abssexg  4622  imassrn  5336  fvclss  6129  fabexg  6729  f1oabexg  6732  mapex  7418  tc2  8164  hta  8306  infmap2  8589  cflm  8621  cflim2  8634  hsmex3  8805  domtriomlem  8813  axdc3lem2  8822  brdom7disj  8900  brdom6disj  8901  npex  9353  hashf1lem2  12489  issubc  15323  isghm  16466  symgbasfi  16610  tgval  19623  ustfn  20870  ustval  20871  ustn0  20889  birthdaylem1  23479  wlks  24721  trls  24740  mptctf  27774  measbase  28405  measval  28406  ismeas  28407  isrnmeas  28408  ballotlem2  28691  subfaclefac  28884  dfon2lem2  29456  sdclem2  30475  eldiophb  30929  hbtlem1  31313  hbtlem7  31315  rabexgf  31639  relopabVD  34102  lineset  35859  lautset  36203  pautsetN  36219  tendoset  36882
  Copyright terms: Public domain W3C validator