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

Theorem ss2abdv 3540
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 1766 . 2  |-  ( ph  ->  A. x ( ps 
->  ch ) )
3 ss2ab 3535 . 2  |-  ( { x  |  ps }  C_ 
{ x  |  ch } 
<-> 
A. x ( ps 
->  ch ) )
42, 3sylibr 215 1  |-  ( ph  ->  { x  |  ps }  C_  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1435   {cab 2414    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-in 3449  df-ss 3456
This theorem is referenced by:  intss  4279  ssopab2  4747  opabbrexOLD  6348  ssoprab2  6361  suppimacnvss  6935  suppimacnv  6936  ressuppss  6945  ss2ixp  7543  fiss  7944  tcss  8227  tcel  8228  infmap2  8646  cfub  8677  cflm  8678  cflecard  8681  clsslem  13027  cncmet  22183  plyss  23021  ofrn2  28081  sigaclci  28793  subfacp1lem6  29696  ss2mcls  29994  itg2addnclem  31696  sdclem1  31775  istotbnd3  31806  sstotbnd  31810  aomclem4  35620  hbtlem4  35690  hbtlem3  35691  rngunsnply  35737  iocinico  35794
  Copyright terms: Public domain W3C validator