Theorem abssdv 3676

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

Step	Hyp	Ref	Expression
1		abssdv.1	. . 3 |- ( ph -> ( ps -> x e. A ) )
2	1	alrimiv 1855	. 2 |- ( ph -> A. x ( ps -> x e. A ) )
3		abss 3671	. 2 |- ( { x | ps } C_ A <-> A. x ( ps -> x e. A ) )
4	2, 3	sylibr 224	1 |- ( ph -> { x | ps } C_ A )

Syntax hints:   -> wi 4   A.wal 1481   e. wcel 1990   {cab 2608   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-in 3581  df-ss 3588

This theorem is referenced by:  dfopif  4399  opabssxpd  5338  fmpt  6381  eroprf  7845  cfslb2n  9090  rankcf  9599  genpv  9821  genpdm  9824  fimaxre3  10970  supadd  10991  supmul  10995  hashfacen  13238  hashf1lem1  13239  hashf1lem2  13240  mertenslem2  14617  4sqlem11  15659  symgbas  17800  lss1d  18963  lspsn  19002  lpval  20943  lpsscls  20945  ptuni2  21379  ptbasfi  21384  prdstopn  21431  xkopt  21458  tgpconncompeqg  21915  metrest  22329  mbfeqalem  23409  limcfval  23636  nmosetre  27619  nmopsetretALT  28722  nmfnsetre  28736  sigaclcuni  30181  bnj849  30995  deranglem  31148  derangsn  31152  nosupno  31849  nosupbday  31851  liness  32252  mblfinlem3  33448  ismblfin  33450  itg2addnclem  33461  areacirclem2  33501  sdclem2  33538  sdclem1  33539  ismtyval  33599  heibor1lem  33608  heibor1  33609  pmapglbx  35055  eldiophb  37320  hbtlem2  37694  upbdrech  39519