Theorem ss2ab

Description: Class abstractions in a subclass relationship. (Contributed by NM, 3-Jul-1994)

	Ref	Expression
Assertion	ss2ab	|- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		nfab1	|- F/_ x { x | ph }
2		nfab1	|- F/_ x { x | ps }
3	1 2	dfss2f	|- ( { x | ph } C_ { x | ps } <-> A. x ( x e. { x | ph } -> x e. { x | ps } ) )
4		abid	|- ( x e. { x | ph } <-> ph )
5		abid	|- ( x e. { x | ps } <-> ps )
6	4 5	imbi12i	|- ( ( x e. { x | ph } -> x e. { x | ps } ) <-> ( ph -> ps ) )
7	6	albii	|- ( A. x ( x e. { x | ph } -> x e. { x | ps } ) <-> A. x ( ph -> ps ) )
8	3 7	bitri	|- ( { x | ph } C_ { x | ps } <-> A. x ( ph -> ps ) )