Metamath Proof Explorer

Theorem ssrab2f

Description: Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ssrab2f.1 
|- F/_ x A
Assertion ssrab2f 
|- { x e. A | ph } C_ A

Proof

Step Hyp Ref Expression
1 ssrab2f.1 
 |-  F/_ x A
2 nfrab1 
 |-  F/_ x { x e. A | ph }
3 2 1 dfss3f 
 |-  ( { x e. A | ph } C_ A <-> A. x e. { x e. A | ph } x e. A )
4 rabidim1 
 |-  ( x e. { x e. A | ph } -> x e. A )
5 3 4 mprgbir 
 |-  { x e. A | ph } C_ A