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

Theorem ss2abdv 3259
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
Hypothesis
Ref Expression
ss2abdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ss2abdv  |-  ( ph  ->  { x  |  ps }  C_  { x  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem ss2abdv
StepHypRef Expression
1 ss2abdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21alrimiv 1621 . 2  |-  ( ph  ->  A. x ( ps 
->  ch ) )
3 ss2ab 3254 . 2  |-  ( { x  |  ps }  C_ 
{ x  |  ch } 
<-> 
A. x ( ps 
->  ch ) )
42, 3sylibr 203 1  |-  ( ph  ->  { x  |  ps }  C_  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   {cab 2282    C_ wss 3165
This theorem is referenced by:  ssopab2  4306  ssoprab2  5920  ss2ixp  6845  fiss  7193  tcss  7445  tcel  7446  infmap2  7860  cfub  7891  cflm  7892  cflecard  7895  cncmet  18760  plyss  19597  ofrn2  23222  sigaclci  23508  subfacp1lem6  23731  itg2addnclem  25003  sdclem1  26556  istotbnd3  26598  sstotbnd  26602  aomclem4  27257  hbtlem4  27433  hbtlem3  27434  rngunsnply  27481  opabbrex  28191
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator