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

Metamath Proof Explorer

Theorem tsksn

Description: A singleton of an element of a Tarski class belongs to the class. JFM CLASSES2 th. 2 (partly). (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 18-Jun-2013)

		Ref	Expression
	Assertion	tsksn	$⊢ (T \in Tarski \land A \in T) \to \{A\} \in T$

Proof

Step	Hyp	Ref	Expression
1		tskpw	$⊢ (T \in Tarski \land A \in T) \to 𝒫 A \in T$
2		snsspw	$⊢ \{A\} \subseteq 𝒫 A$
3		tskss	$⊢ (T \in Tarski \land 𝒫 A \in T \land \{A\} \subseteq 𝒫 A) \to \{A\} \in T$
4	2 3	mp3an3	$⊢ (T \in Tarski \land 𝒫 A \in T) \to \{A\} \in T$
5	1 4	syldan	$⊢ (T \in Tarski \land A \in T) \to \{A\} \in T$