Theorem ss2ab 2119

Description: Class abstractions in a subclass relationship.

Assertion

Ref	Expression
ss2ab	|- ({x | ph} (_ {x | ps} <-> A.x(ph -> ps))

Proof of Theorem ss2ab

Step	Hyp	Ref	Expression
1		hbab1 1469	. . 3 |- (y e. {x | ph} -> A.x y e. {x | ph})
2		hbab1 1469	. . 3 |- (y e. {x | ps} -> A.x y e. {x | ps})
3	1, 2	dfss2f 2063	. 2 |- ({x | ph} (_ {x | ps} <-> A.x(x e. {x | ph} -> x e. {x | ps}))
4		abid 1468	. . . 4 |- (x e. {x | ph} <-> ph)
5		abid 1468	. . . 4 |- (x e. {x | ps} <-> ps)
6	4, 5	imbi12i 188	. . 3 |- ((x e. {x | ph} -> x e. {x | ps}) <-> (ph -> ps))
7	6	albii 1001	. 2 |- (A.x(x e. {x | ph} -> x e. {x | ps}) <-> A.x(ph -> ps))
8	3, 7	bitr 173	1 |- ({x | ph} (_ {x | ps} <-> A.x(ph -> ps))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 956   e. wcel 960  {cab 1466   (_ wss 2050

This theorem is referenced by:  abss 2120  ssab 2121  ss2abi 2123  ss2rab 2126  rabss2 2132  uniss 2525  iunss1 2578  ssopab2 2828  mapss 4352  cfub 4920  cflim 4921  cflecard 4924  lpval 7740  homeofval 10502

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