Theorem ss2abi 3320

Description: Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.)

Hypothesis

Ref	Expression
ss2abi.1	|- ( ph -> ps )

Assertion

Ref	Expression
ss2abi	|- { x | ph } C_ { x | ps }

Proof of Theorem ss2abi

Step	Hyp	Ref	Expression
1		ss2ab 3316	. 2 |- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )
2		ss2abi.1	. 2 |- ( ph -> ps )
3	1, 2	mpgbir 1506	1 |- { x | ph } C_ { x | ps }

Syntax hints:   -> wi 4   {cab 2224   C_ wss 3220

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-in 3226  df-ss 3233

This theorem is referenced by:  abssi  3323  rabssab  3337  abanssl  3501  abanssr  3502  pwsnss  3924  iinuniss  4090  pwpwssunieq  4096  abssexg  4314  imassrn  5132  imadiflem  5455  imainlem  5457  fabexg  5574  f1oabexg  5646  tfrcllemssrecs  6613  mapex  6918  f1setfi  7307  ballotfilem2  13206  tgval  13593  tgvalex  13594  fngzsum  13685  gzsumvalx  13686  isghm  14023  wksfval  16477