Theorem tskin

Description: The intersection of two elements of a Tarski class belongs to the class. (Contributed by FL, 30-Dec-2010) (Proof shortened by Mario Carneiro, 20-Sep-2014)

	Ref	Expression
Assertion	tskin	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
2		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑇 )
3	1 2	mp3an3	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝑇 )