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

Theorem abssdv 3579
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 1695 . 2  |-  ( ph  ->  A. x ( ps 
->  x  e.  A
) )
3 abss 3574 . 2  |-  ( { x  |  ps }  C_  A  <->  A. x ( ps 
->  x  e.  A
) )
42, 3sylibr 212 1  |-  ( ph  ->  { x  |  ps }  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377    e. wcel 1767   {cab 2452    C_ wss 3481
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 3488  df-ss 3495
This theorem is referenced by:  dfopif  4216  fmpt  6053  eroprf  7421  cfslb2n  8660  rankcf  9167  gruiun  9189  genpv  9389  genpdm  9392  fimaxre3  10504  supmul  10523  hashfacen  12484  hashf1lem1  12485  hashf1lem2  12486  swrd0  12638  mertenslem2  13674  4sqlem11  14349  symgbas  16277  lss1d  17480  lspsn  17519  lpval  19508  lpsscls  19510  ptuni2  19945  ptbasfi  19950  prdstopn  19997  xkopt  20024  tgpconcompeqg  20478  metrest  20895  mbfeqalem  21917  limcfval  22144  nmosetre  25502  nmopsetretALT  26605  nmfnsetre  26619  sigaclcuni  27943  deranglem  28435  derangsn  28439  liness  29722  supadd  29969  mblfinlem3  29980  ismblfin  29982  itg2addnclem  29993  areacirclem2  30035  sdclem2  30162  sdclem1  30163  ismtyval  30223  heibor1lem  30232  heibor1  30233  eldiophb  30618  hbtlem2  31001  bnj849  33463  pmapglbx  34966
  Copyright terms: Public domain W3C validator