Theorem ssrabdv

Description: Subclass of a restricted class abstraction (deduction form). (Contributed by NM, 31-Aug-2006)

	Ref	Expression
Hypotheses	ssrabdv.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	ssrabdv.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
Assertion	ssrabdv	⊢ ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		ssrabdv.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
2		ssrabdv.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝜓 )
3	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝜓 )
4		ssrab	⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
5	1 3 4	sylanbrc	⊢ ( 𝜑 → 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜓 } )