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

Theorem abssdv 3537
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 1686 . 2  |-  ( ph  ->  A. x ( ps 
->  x  e.  A
) )
3 abss 3532 . 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 1368    e. wcel 1758   {cab 2439    C_ wss 3439
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 1955  ax-ext 2432
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 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3446  df-ss 3453
This theorem is referenced by:  dfopif  4167  fmpt  5976  eroprf  7311  cfslb2n  8552  rankcf  9059  gruiun  9081  genpv  9283  genpdm  9286  fimaxre3  10394  supmul  10413  hashfacen  12329  hashf1lem1  12330  hashf1lem2  12331  swrd0  12449  mertenslem2  13467  4sqlem11  14138  symgbas  16008  lss1d  17177  lspsn  17216  lpval  18885  lpsscls  18887  ptuni2  19291  ptbasfi  19296  prdstopn  19343  xkopt  19370  tgpconcompeqg  19824  metrest  20241  mbfeqalem  21263  limcfval  21490  nmosetre  24343  nmopsetretALT  25446  nmfnsetre  25460  sigaclcuni  26729  deranglem  27221  derangsn  27225  liness  28343  supadd  28589  mblfinlem3  28601  ismblfin  28603  itg2addnclem  28614  areacirclem2  28656  sdclem2  28809  sdclem1  28810  ismtyval  28870  heibor1lem  28879  heibor1  28880  eldiophb  29266  hbtlem2  29651  bnj849  32273  pmapglbx  33776
  Copyright terms: Public domain W3C validator