Theorem tsk1

Description: One is an element of a nonempty Tarski class. (Contributed by FL, 22-Feb-2011)

	Ref	Expression
Assertion	tsk1	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 1o ∈ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2		tsk0	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ∅ ∈ 𝑇 )
3		tsksn	⊢ ( ( 𝑇 ∈ Tarski ∧ ∅ ∈ 𝑇 ) → { ∅ } ∈ 𝑇 )
4	2 3	syldan	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → { ∅ } ∈ 𝑇 )
5	1 4	eqeltrid	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 1o ∈ 𝑇 )