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 }

This proof depends on syntax axioms:   -> wi 4   {cab 2224   C_ wss 3220

This proof depends on 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 proof 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 used by:  abssi  3323  rabssab  3337  abanssl  3501  abanssr  3502  pwsnss  3929  iinuniss  4095  pwpwssunieq  4101  abssexg  4319  imassrn  5137  imadiflem  5460  imainlem  5462  fabexg  5579  f1oabexg  5651  tfrcllemssrecs  6623  mapex  6928  f1setfi  7317  ballotfilem2  13228  tgval  13616  tgvalex  13617  fngzsum  13708  gzsumvalx  13709  isghm  14046  birthdaylem1g  16087  wksfval  16563