Theorem ssrab

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

	Ref	Expression
Assertion	ssrab	⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2	1	sseq2i	⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ 𝐵 ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } )
3		ssab	⊢ ( 𝐵 ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
4		dfss3	⊢ ( 𝐵 ⊆ 𝐴 ↔ ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 )
5	4	anbi1i	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )
6		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )
7		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
8	5 6 7	3bitr2ri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )
9	2 3 8	3bitri	⊢ ( 𝐵 ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝐵 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) )