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	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to A\cap B\in T$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap B\subseteq A$$
2		tskss	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\wedge A\cap B\subseteq A\right)\to A\cap B\in T$$
3	1 2	mp3an3	$$⊢\left(T\in \mathrm{Tarski}\wedge A\in T\right)\to A\cap B\in T$$