Theorem tsk1

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

	Ref	Expression
Assertion	tsk1	|- ( ( T e. Tarski /\ T =/= (/) ) -> 1o e. T )

Proof

Step	Hyp	Ref	Expression
1		df1o2	|- 1o = { (/) }
2		tsk0	|- ( ( T e. Tarski /\ T =/= (/) ) -> (/) e. T )
3		tsksn	|- ( ( T e. Tarski /\ (/) e. T ) -> { (/) } e. T )
4	2 3	syldan	|- ( ( T e. Tarski /\ T =/= (/) ) -> { (/) } e. T )
5	1 4	eqeltrid	|- ( ( T e. Tarski /\ T =/= (/) ) -> 1o e. T )