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

Theorem ss2abdv 3528
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 1686 . 2  |-  ( ph  ->  A. x ( ps 
->  ch ) )
3 ss2ab 3523 . 2  |-  ( { x  |  ps }  C_ 
{ x  |  ch } 
<-> 
A. x ( ps 
->  ch ) )
42, 3sylibr 212 1  |-  ( ph  ->  { x  |  ps }  C_  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368   {cab 2437    C_ wss 3431
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 1954  ax-ext 2431
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 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-in 3438  df-ss 3445
This theorem is referenced by:  ssopab2  4717  opabbrex  6234  ssoprab2  6246  suppimacnvss  6805  suppimacnv  6806  ressuppss  6813  ss2ixp  7381  fiss  7780  tcss  8070  tcel  8071  infmap2  8493  cfub  8524  cflm  8525  cflecard  8528  cncmet  20960  plyss  21795  ofrn2  26104  sigaclci  26715  subfacp1lem6  27212  itg2addnclem  28586  sdclem1  28782  istotbnd3  28813  sstotbnd  28817  aomclem4  29553  hbtlem4  29625  hbtlem3  29626  rngunsnply  29673  iocinico  29730
  Copyright terms: Public domain W3C validator