Theorem ss2abi 2123

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

Syntax hints:   -> wi 3  {cab 1466   (_ wss 2050

This theorem is referenced by:  abssi 2125  opabss 2673  intabs 2738  moabex 2772  dmcoss 3369  imassrn 3421  fabexg 3659  f1oabexg 3706  tz6.12-2 3745  fvclss 3861  abrexexlem1 3864  abrexex 3866  mapex 4334  mapsspw 4347  pw2en 4452  hta 4738  aceq3lem 4742  aceq5lem4 4748  aceq6b 4752  brdom7disj 4814  brdom6disj 4815  cflim 4921  cfom 4928  npex 5103  sumex 6981  cncfval 7264  infxpidmlem9 7561  infmap2lem2 7582  infmap2 7583  gch-kn 7589  tgvalt 7615  cncnplem1 7771  opnfss 7855  issubg 8112  nvvcop 8209  shex 9072

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056

Copyright terms: Public domain