Metamath Proof Explorer

Theorem ssab2

Description: Subclass relation for the restriction of a class abstraction. (Contributed by NM, 31-Mar-1995)

Ref Expression
Assertion ssab2 
|- { x | ( x e. A /\ ph ) } C_ A

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( x e. A /\ ph ) -> x e. A )
2 1 abssi 
 |-  { x | ( x e. A /\ ph ) } C_ A