Theorem bj-gabssd

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

	Ref	Expression
Hypotheses	bj-gabssd.nf	|- ( ph -> A. x ph )
	bj-gabssd.c	|- ( ph -> A = B )
	bj-gabssd.f	|- ( ph -> ( ps -> ch ) )
Assertion	bj-gabssd	|- ( ph -> {{ A | x | ps }} C_ {{ B | x | ch }} )

Proof

Step	Hyp	Ref	Expression
1		bj-gabssd.nf	|- ( ph -> A. x ph )
2		bj-gabssd.c	|- ( ph -> A = B )
3		bj-gabssd.f	|- ( ph -> ( ps -> ch ) )
4	2 3	jca	|- ( ph -> ( A = B /\ ( ps -> ch ) ) )
5	1 4	alrimih	|- ( ph -> A. x ( A = B /\ ( ps -> ch ) ) )
6		bj-gabss	|- ( A. x ( A = B /\ ( ps -> ch ) ) -> {{ A | x | ps }} C_ {{ B | x | ch }} )
7	5 6	syl	|- ( ph -> {{ A | x | ps }} C_ {{ B | x | ch }} )