Theorem ss2abdv 3675

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)

Hypothesis

Ref	Expression
ss2abdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
ss2abdv	|- ( ph -> { x | ps } C_ { x | ch } )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem ss2abdv

Step	Hyp	Ref	Expression
1		ss2abdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	alrimiv 1855	. 2 |- ( ph -> A. x ( ps -> ch ) )
3		ss2ab 3670	. 2 |- ( { x | ps } C_ { x | ch } <-> A. x ( ps -> ch ) )
4	2, 3	sylibr 224	1 |- ( ph -> { x | ps } C_ { x | ch } )

Syntax hints:   -> wi 4   A.wal 1481   {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:  intss  4498  ssopab2  5001  ssoprab2  6711  suppimacnvss  7305  suppimacnv  7306  ressuppss  7314  ss2ixp  7921  fiss  8330  tcss  8620  tcel  8621  infmap2  9040  cfub  9071  cflm  9072  cflecard  9075  clsslem  13723  cncmet  23119  plyss  23955  ofrn2  29442  sigaclci  30195  subfacp1lem6  31167  ss2mcls  31465  itg2addnclem  33461  sdclem1  33539  istotbnd3  33570  sstotbnd  33574  qsss1  34053  aomclem4  37627  hbtlem4  37696  hbtlem3  37697  rngunsnply  37743  iocinico  37797