# Metamath Proof Explorer

## Theorem ss2rab

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

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

### Proof

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