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

Theorem abssdv 3247
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
Hypothesis
Ref Expression
abssdv.1  |-  ( ph  ->  ( ps  ->  x  e.  A ) )
Assertion
Ref Expression
abssdv  |-  ( ph  ->  { x  |  ps }  C_  A )
Distinct variable groups:    ph, x    x, A
Allowed substitution hint:    ps( x)

Proof of Theorem abssdv
StepHypRef Expression
1 abssdv.1 . . 3  |-  ( ph  ->  ( ps  ->  x  e.  A ) )
21alrimiv 1617 . 2  |-  ( ph  ->  A. x ( ps 
->  x  e.  A
) )
3 abss 3242 . 2  |-  ( { x  |  ps }  C_  A  <->  A. x ( ps 
->  x  e.  A
) )
42, 3sylibr 203 1  |-  ( ph  ->  { x  |  ps }  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    e. wcel 1684   {cab 2269    C_ wss 3152
This theorem is referenced by:  dfopif  3793  fmpt  5681  eroprf  6756  cfslb2n  7894  rankcf  8399  gruiun  8421  genpv  8623  genpdm  8626  fimaxre3  9703  supmul  9722  hashfacen  11392  hashf1lem1  11393  hashf1lem2  11394  mertenslem2  12341  4sqlem11  13002  symgbas  14772  lss1d  15720  lspsn  15759  lpval  16871  lpsscls  16873  ptuni2  17271  ptbasfi  17276  prdstopn  17322  xkopt  17349  tgpconcompeqg  17794  metrest  18070  mbfeqalem  18997  limcfval  19222  nmosetre  21342  nmopsetretALT  22443  nmfnsetre  22457  deranglem  23697  derangsn  23701  liness  24768  areacirclem4  24927  intopcoaconb  25540  sdclem2  26452  sdclem1  26453  ismtyval  26524  heibor1lem  26533  heibor1  26534  eldiophb  26836  hbtlem2  27328  bnj849  28957  pmapglbx  29958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator