Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal representation of numbers
1eltp012
Next ⟩
0ne1
Metamath Proof Explorer
Ascii
Unicode
Theorem
1eltp012
Description:
1 is an element of
{ 0 , 1 , 2 }
.
(Contributed by
Umit Teoman Dogan
, 10-Jun-2026)
Ref
Expression
Assertion
1eltp012
⊢
1
∈
0
1
2
Proof
Step
Hyp
Ref
Expression
1
1ex
⊢
1
∈
V
2
1
tpid2
⊢
1
∈
0
1
2