Theorem ss2rabd

Description: Subclass of a restricted class abstraction (deduction form). Saves ax-10 , ax-11 , ax-12 over using ss2rab and sylibr . (Contributed by SN, 4-Feb-2026)

	Ref	Expression
Hypothesis	ss2rabd.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) )
Assertion	ss2rabd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		ss2rabd.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
3		imdistan	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
4	3	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
5	2 4	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜒 ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
6	1 5	sylib	⊢ ( 𝜑 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
7		ss2abim	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } )
8	6 7	syl	⊢ ( 𝜑 → { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) } )
9		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) }
10		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜒 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) }
11	8 9 10	3sstr4g	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜒 } )