Metamath Proof Explorer

Theorem ssrab2

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997)

Ref Expression
Assertion ssrab2 
|- { x e. A | ph } C_ A

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
2 ssab2 
 |-  { x | ( x e. A /\ ph ) } C_ A
3 1 2 eqsstri 
 |-  { x e. A | ph } C_ A