Theorem ss2rab 3086

Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)

Assertion

Ref	Expression
ss2rab	|- ( { x e. A | ph } C_ { x e. A | ps } <-> A. x e. A ( ph -> ps ) )

Proof of Theorem ss2rab

Step	Hyp	Ref	Expression
1		df-rab 2364	. . 3 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		df-rab 2364	. . 3 |- { x e. A | ps } = { x | ( x e. A /\ ps ) }
3	1, 2	sseq12i 3041	. 2 |- ( { x e. A | ph } C_ { x e. A | ps } <-> { x | ( x e. A /\ ph ) } C_ { x | ( x e. A /\ ps ) } )
4		ss2ab 3078	. 2 |- ( { x | ( x e. A /\ ph ) } C_ { x | ( x e. A /\ ps ) } <-> A. x ( ( x e. A /\ ph ) -> ( x e. A /\ ps ) ) )
5		df-ral 2360	. . 3 |- ( A. x e. A ( ph -> ps ) <-> A. x ( x e. A -> ( ph -> ps ) ) )
6		imdistan 433	. . . 4 |- ( ( x e. A -> ( ph -> ps ) ) <-> ( ( x e. A /\ ph ) -> ( x e. A /\ ps ) ) )
7	6	albii 1402	. . 3 |- ( A. x ( x e. A -> ( ph -> ps ) ) <-> A. x ( ( x e. A /\ ph ) -> ( x e. A /\ ps ) ) )
8	5, 7	bitr2i 183	. 2 |- ( A. x ( ( x e. A /\ ph ) -> ( x e. A /\ ps ) ) <-> A. x e. A ( ph -> ps ) )
9	3, 4, 8	3bitri 204	1 |- ( { x e. A | ph } C_ { x e. A | ps } <-> A. x e. A ( ph -> ps ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   A.wal 1285   e. wcel 1436   {cab 2071   A.wral 2355   {crab 2359   C_ wss 2988

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rab 2364  df-in 2994  df-ss 3001

This theorem is referenced by:  ss2rabdv  3091  ss2rabi  3092