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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → { 𝐴 } ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		tskpw	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → 𝒫 𝐴 ∈ 𝑇 )
2		snsspw	⊢ { 𝐴 } ⊆ 𝒫 𝐴
3		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝒫 𝐴 ∈ 𝑇 ∧ { 𝐴 } ⊆ 𝒫 𝐴 ) → { 𝐴 } ∈ 𝑇 )
4	2 3	mp3an3	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝒫 𝐴 ∈ 𝑇 ) → { 𝐴 } ∈ 𝑇 )
5	1 4	syldan	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇 ) → { 𝐴 } ∈ 𝑇 )