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

Metamath Proof Explorer

Theorem tsk1

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

		Ref	Expression
	Assertion	tsk1	$⊢ (T \in Tarski \land T \neq \emptyset) \to 1_{𝑜} \in T$

Step	Hyp	Ref	Expression
1		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
2		tsk0	$⊢ (T \in Tarski \land T \neq \emptyset) \to \emptyset \in T$
3		tsksn	$⊢ (T \in Tarski \land \emptyset \in T) \to \{\emptyset\} \in T$
4	2 3	syldan	$⊢ (T \in Tarski \land T \neq \emptyset) \to \{\emptyset\} \in T$
5	1 4	eqeltrid	$⊢ (T \in Tarski \land T \neq \emptyset) \to 1_{𝑜} \in T$