Theorem ssrabdf

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	ssrabdf.1	⊢ Ⅎ 𝑥 𝐴
	ssrabdf.2	⊢ Ⅎ 𝑥 𝐵
	ssrabdf.3	⊢ Ⅎ 𝑥 𝜑
	ssrabdf.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	ssrabdf.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
Assertion	ssrabdf	⊢ ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		ssrabdf.1	⊢ Ⅎ 𝑥 𝐴
2		ssrabdf.2	⊢ Ⅎ 𝑥 𝐵
3		ssrabdf.3	⊢ Ⅎ 𝑥 𝜑
4		ssrabdf.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
5		ssrabdf.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
6	3 5	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝜓 )
7	2 1	ssrabf	⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
8	4 6 7	sylanbrc	⊢ ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )