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 Tarski T 1 𝑜 T

Proof

Step Hyp Ref Expression
1 df1o2 1 𝑜 =
2 tsk0 T Tarski T T
3 tsksn T Tarski T T
4 2 3 syldan T Tarski T T
5 1 4 eqeltrid T Tarski T 1 𝑜 T