Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal representation of numbers
1eltp012
Next ⟩
0ne1
Metamath Proof Explorer
Ascii
Structured
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 }