Metamath Proof Explorer

Theorem ssrab2

Description: Subclass relation for a restricted class. (Contributed by NM, 19-Mar-1997) (Proof shortened by BJ and SN, 8-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 elrabi 
 |-  ( y e. { x e. A | ph } -> y e. A )
2 1 ssriv 
 |-  { x e. A | ph } C_ A