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

Theorem abssdv 3414
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 1684 . 2  |-  ( ph  ->  A. x ( ps 
->  x  e.  A
) )
3 abss 3409 . 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 1360    e. wcel 1755   {cab 2419    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-in 3323  df-ss 3330
This theorem is referenced by:  dfopif  4044  fmpt  5852  eroprf  7186  cfslb2n  8425  rankcf  8932  gruiun  8954  genpv  9156  genpdm  9159  fimaxre3  10267  supmul  10286  hashfacen  12191  hashf1lem1  12192  hashf1lem2  12193  swrd0  12311  mertenslem2  13328  4sqlem11  13999  symgbas  15865  lss1d  16966  lspsn  17005  lpval  18585  lpsscls  18587  ptuni2  18991  ptbasfi  18996  prdstopn  19043  xkopt  19070  tgpconcompeqg  19524  metrest  19941  mbfeqalem  20962  limcfval  21189  nmosetre  23987  nmopsetretALT  25090  nmfnsetre  25104  sigaclcuni  26415  deranglem  26902  derangsn  26906  liness  28023  supadd  28262  mblfinlem3  28274  ismblfin  28276  itg2addnclem  28287  areacirclem2  28329  sdclem2  28482  sdclem1  28483  ismtyval  28543  heibor1lem  28552  heibor1  28553  eldiophb  28940  hbtlem2  29325  bnj849  31641  pmapglbx  33007
  Copyright terms: Public domain W3C validator