Theorem ss2abi 1552

Description: Inference of abstraction subclass from implication.

Hypothesis

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

Assertion

Ref	Expression
ss2abi	|- {x | ph} (_ {x | ps}

Proof of Theorem ss2abi

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

Syntax hints:   -> wi 2  {cab 1090   (_ wss 1487

This theorem is referenced by:  ssab 1555  moabex 1868  opabss 2100  dmexg 2551  rnexg 2569  dmco 2570  imassrn 2611  tz6.12-2 2845  fvclss 2907  abrexexlem1 2910  abrexex 2912  mapex 3261  pw2en 3348  aceq3lem 3555  aceq5lem4 3561  aceq6b 3565  hta 3619  cflim 3704  cfsuc 3709  cfom 3710  npex 3885  nnind 4434  infxpidmlem9 4941  infmap2lem2 4952  infmap2 4953  gch-kn 4957  shex 5115

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org