Theorem bj-gabss

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

	Ref	Expression
Assertion	bj-gabss	⊢ ( ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → { 𝐴 ∣ 𝑥 ∣ 𝜑 } ⊆ { 𝐵 ∣ 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = 𝑦 ↔ 𝐵 = 𝑦 ) )
2	1	biimpd	⊢ ( 𝐴 = 𝐵 → ( 𝐴 = 𝑦 → 𝐵 = 𝑦 ) )
3	2	adantr	⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝐴 = 𝑦 → 𝐵 = 𝑦 ) )
4		simpr	⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 → 𝜓 ) )
5	3 4	anim12d	⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → ( ( 𝐴 = 𝑦 ∧ 𝜑 ) → ( 𝐵 = 𝑦 ∧ 𝜓 ) ) )
6	5	aleximi	⊢ ( ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → ( ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) → ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ) )
7	6	alrimiv	⊢ ( ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → ∀ 𝑦 ( ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) → ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ) )
8		ss2ab	⊢ ( { 𝑦 ∣ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) } ⊆ { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) } ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) → ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) ) )
9	7 8	sylibr	⊢ ( ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → { 𝑦 ∣ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) } ⊆ { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) } )
10		df-bj-gab	⊢ { 𝐴 ∣ 𝑥 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ( 𝐴 = 𝑦 ∧ 𝜑 ) }
11		df-bj-gab	⊢ { 𝐵 ∣ 𝑥 ∣ 𝜓 } = { 𝑦 ∣ ∃ 𝑥 ( 𝐵 = 𝑦 ∧ 𝜓 ) }
12	9 10 11	3sstr4g	⊢ ( ∀ 𝑥 ( 𝐴 = 𝐵 ∧ ( 𝜑 → 𝜓 ) ) → { 𝐴 ∣ 𝑥 ∣ 𝜑 } ⊆ { 𝐵 ∣ 𝑥 ∣ 𝜓 } )