Theorem tskss

Description: The subsets of an element of a Tarski class belong to the class. (Contributed by FL, 30-Dec-2010) (Revised by Mario Carneiro, 18-Jun-2013)

	Ref	Expression
Assertion	tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		elpw2g	⊢ ( 𝐴 ∈ 𝑇 → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
2	1	adantl	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
3		tskpwss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ⊆ 𝑇 )
4	3	sseld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐵 ∈ 𝒫 𝐴 → 𝐵 ∈ 𝑇 ) )
5	2 4	sylbird	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ 𝑇 ) )
6	5	3impia	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝑇 )