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

Theorem ss2abdv 3573
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 1695 . 2  |-  ( ph  ->  A. x ( ps 
->  ch ) )
3 ss2ab 3568 . 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 1377   {cab 2452    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490
This theorem is referenced by:  ssopab2  4773  opabbrex  6322  ssoprab2  6335  suppimacnvss  6908  suppimacnv  6909  ressuppss  6916  ss2ixp  7479  fiss  7880  tcss  8171  tcel  8172  infmap2  8594  cfub  8625  cflm  8626  cflecard  8629  cncmet  21496  plyss  22331  ofrn2  27153  sigaclci  27772  subfacp1lem6  28269  itg2addnclem  29643  sdclem1  29839  istotbnd3  29870  sstotbnd  29874  aomclem4  30607  hbtlem4  30679  hbtlem3  30680  rngunsnply  30727  iocinico  30784
  Copyright terms: Public domain W3C validator