Metamath Proof Explorer

Theorem ssrab2OLD

Description: Obsolete version of ssrab2 as of 8-Aug-2024. (Contributed by NM, 19-Mar-1997) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion ssrab2OLD 
|- { 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