Theorem bj-gabssd

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

	Ref	Expression
Hypotheses	bj-gabssd.nf	$$⊢\phi \to \forall x\phi$$
	bj-gabssd.c	$$⊢\phi \to A=B$$
	bj-gabssd.f	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	bj-gabssd	$$⊢\phi \to {{A\left|x\right|\psi }}\subseteq {{B\left|x\right|\chi }}$$

Proof

Step	Hyp	Ref	Expression
1		bj-gabssd.nf	$$⊢\phi \to \forall x\phi$$
2		bj-gabssd.c	$$⊢\phi \to A=B$$
3		bj-gabssd.f	$$⊢\phi \to \left(\psi \to \chi \right)$$
4	2 3	jca	$$⊢\phi \to \left(A=B\wedge \left(\psi \to \chi \right)\right)$$
5	1 4	alrimih	$$⊢\phi \to \forall x\left(A=B\wedge \left(\psi \to \chi \right)\right)$$
6		bj-gabss	$$⊢\forall x\left(A=B\wedge \left(\psi \to \chi \right)\right)\to {{A\left|x\right|\psi }}\subseteq {{B\left|x\right|\chi }}$$
7	5 6	syl	$$⊢\phi \to {{A\left|x\right|\psi }}\subseteq {{B\left|x\right|\chi }}$$