Theorem ss2abi 3674

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 3670	. 2 |- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )
2		ss2abi.1	. 2 |- ( ph -> ps )
3	1, 2	mpgbir 1726	1 |- { x | ph } C_ { x | ps }

Syntax hints:   -> wi 4   {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:  abssi  3677  rabssab  3690  pwpwssunieq  4615  intabs  4825  abssexg  4851  imassrn  5477  fvclss  6500  fabexg  7122  f1oabexg  7125  mapex  7863  tc2  8618  hta  8760  infmap2  9040  cflm  9072  cflim2  9085  hsmex3  9256  domtriomlem  9264  axdc3lem2  9273  brdom7disj  9353  brdom6disj  9354  npex  9808  hashf1lem2  13240  issubc  16495  isghm  17660  symgbasfi  17806  tgval  20759  ustfn  22005  ustval  22006  ustn0  22024  birthdaylem1  24678  rgrprc  26487  wksfval  26505  mptctf  29495  measbase  30260  measval  30261  ismeas  30262  isrnmeas  30263  ballotlem2  30550  subfaclefac  31158  dfon2lem2  31689  nosupno  31849  poimirlem4  33413  poimirlem9  33418  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem32  33441  sdclem2  33538  lineset  35024  lautset  35368  pautsetN  35384  tendoset  36047  eldiophb  37320  hbtlem1  37693  hbtlem7  37695  relopabVD  39137  rabexgf  39183  upwlksfval  41716