Theorem bj-gabss

Description: Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024)

	Ref	Expression
Assertion	bj-gabss	|- ( A. x ( A = B /\ ( ph -> ps ) ) -> {{ A | x | ph }} C_ {{ B | x | ps }} )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	|- ( A = B -> ( A = y <-> B = y ) )
2	1	biimpd	|- ( A = B -> ( A = y -> B = y ) )
3	2	adantr	|- ( ( A = B /\ ( ph -> ps ) ) -> ( A = y -> B = y ) )
4		simpr	|- ( ( A = B /\ ( ph -> ps ) ) -> ( ph -> ps ) )
5	3 4	anim12d	|- ( ( A = B /\ ( ph -> ps ) ) -> ( ( A = y /\ ph ) -> ( B = y /\ ps ) ) )
6	5	aleximi	|- ( A. x ( A = B /\ ( ph -> ps ) ) -> ( E. x ( A = y /\ ph ) -> E. x ( B = y /\ ps ) ) )
7	6	alrimiv	|- ( A. x ( A = B /\ ( ph -> ps ) ) -> A. y ( E. x ( A = y /\ ph ) -> E. x ( B = y /\ ps ) ) )
8		ss2ab	|- ( { y | E. x ( A = y /\ ph ) } C_ { y | E. x ( B = y /\ ps ) } <-> A. y ( E. x ( A = y /\ ph ) -> E. x ( B = y /\ ps ) ) )
9	7 8	sylibr	|- ( A. x ( A = B /\ ( ph -> ps ) ) -> { y | E. x ( A = y /\ ph ) } C_ { y | E. x ( B = y /\ ps ) } )
10		df-bj-gab	|- {{ A | x | ph }} = { y | E. x ( A = y /\ ph ) }
11		df-bj-gab	|- {{ B | x | ps }} = { y | E. x ( B = y /\ ps ) }
12	9 10 11	3sstr4g	|- ( A. x ( A = B /\ ( ph -> ps ) ) -> {{ A | x | ph }} C_ {{ B | x | ps }} )