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	|- ( ( T e. Tarski /\ A e. T ) -> ( A i^i B ) e. T )

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( A i^i B ) C_ A
2		tskss	|- ( ( T e. Tarski /\ A e. T /\ ( A i^i B ) C_ A ) -> ( A i^i B ) e. T )
3	1 2	mp3an3	|- ( ( T e. Tarski /\ A e. T ) -> ( A i^i B ) e. T )