This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in Tarski \land A \in T) \to A \cap B \in T$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ A \cap B \subseteq A$
2		tskss	$⊢ (T \in Tarski \land A \in T \land A \cap B \subseteq A) \to A \cap B \in T$
3	1 2	mp3an3	$⊢ (T \in Tarski \land A \in T) \to A \cap B \in T$