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  4321  imassrn  5140  imadiflem  5463  imainlem  5465  fabexg  5582  f1oabexg  5654  tfrcllemssrecs  6627  mapex  6932  f1setfi  7322  ballotfilem2  13286  tgval  13675  tgvalex  13676  fngzsum  13767  gzsumvalx  13768  isghm  14105  birthdaylem1g  16225  wksfval  16768