Theorem bj-gabssd

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

	Ref	Expression
Hypotheses	bj-gabssd.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	bj-gabssd.c	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	bj-gabssd.f	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	bj-gabssd	⊢ ( 𝜑 → { 𝐴 ∣ 𝑥 ∣ 𝜓 } ⊆ { 𝐵 ∣ 𝑥 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		bj-gabssd.nf	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		bj-gabssd.c	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		bj-gabssd.f	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
4	2 3	jca	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∧ ( 𝜓 → 𝜒 ) ) )
5	1 4	alrimih	⊢ ( 𝜑 → ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜓 → 𝜒 ) ) )
6		bj-gabss	⊢ ( ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜓 → 𝜒 ) ) → { 𝐴 ∣ 𝑥 ∣ 𝜓 } ⊆ { 𝐵 ∣ 𝑥 ∣ 𝜒 } )
7	5 6	syl	⊢ ( 𝜑 → { 𝐴 ∣ 𝑥 ∣ 𝜓 } ⊆ { 𝐵 ∣ 𝑥 ∣ 𝜒 } )