Theorem ss2abi 2116

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 2112	. 2 |- ({x | ph} (_ {x | ps} <-> A.x(ph -> ps))
2		ss2abi.1	. 2 |- (ph -> ps)
3	1, 2	mpgbir 986	1 |- {x | ph} (_ {x | ps}

Syntax hints:   -> wi 3  {cab 1461   (_ wss 2043

This theorem is referenced by:  abssi 2118  opabss 2663  intabs 2728  moabex 2761  dmcoss 3355  imassrn 3407  fabexg 3644  f1oabexg 3691  tz6.12-2 3730  fvclss 3846  abrexexlem1 3849  abrexex 3851  mapex 4318  mapsspw 4331  pw2en 4432  abfii2 4542  abfii4 4544  hta 4708  aceq3lem 4712  aceq5lem4 4718  aceq6b 4722  brdom7disj 4784  brdom6disj 4785  cflim 4889  cfom 4896  npex 5071  sumex 6927  cncfval 7207  infxpidmlem9 7511  infmap2lem2 7530  infmap2 7531  gch-kn 7537  tgvalt 7566  subbas 7594  cncnplem1 7724  opnfss 7810  issubg 8068  nvvcop 8165  shex 9016

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain