Theorem ss2abim

Description: Class abstractions in a subclass relationship. Reverse direction of ss2ab which requires fewer axioms. (Contributed by SN, 2-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		spsbim	|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
2	1	alrimiv	|- ( A. x ( ph -> ps ) -> A. y ( [ y / x ] ph -> [ y / x ] ps ) )
3		df-ss	|- ( { x | ph } C_ { x | ps } <-> A. y ( y e. { x | ph } -> y e. { x | ps } ) )
4		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
5		df-clab	|- ( y e. { x | ps } <-> [ y / x ] ps )
6	4 5	imbi12i	|- ( ( y e. { x | ph } -> y e. { x | ps } ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
7	6	albii	|- ( A. y ( y e. { x | ph } -> y e. { x | ps } ) <-> A. y ( [ y / x ] ph -> [ y / x ] ps ) )
8	3 7	bitr2i	|- ( A. y ( [ y / x ] ph -> [ y / x ] ps ) <-> { x | ph } C_ { x | ps } )
9	2 8	sylib	|- ( A. x ( ph -> ps ) -> { x | ph } C_ { x | ps } )