Metamath Proof Explorer


Theorem ssabf

Description: Subclass of a class abstraction. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ssabf.1
|- F/_ x A
Assertion ssabf
|- ( A C_ { x | ph } <-> A. x ( x e. A -> ph ) )

Proof

Step Hyp Ref Expression
1 ssabf.1
 |-  F/_ x A
2 1 abid2f
 |-  { x | x e. A } = A
3 2 sseq1i
 |-  ( { x | x e. A } C_ { x | ph } <-> A C_ { x | ph } )
4 ss2ab
 |-  ( { x | x e. A } C_ { x | ph } <-> A. x ( x e. A -> ph ) )
5 3 4 bitr3i
 |-  ( A C_ { x | ph } <-> A. x ( x e. A -> ph ) )