Metamath Proof Explorer


Theorem fz01pr

Description: An integer range between 0 and 1 is a pair. (Contributed by AV, 11-Sep-2025)

Ref Expression
Assertion fz01pr ( 0 ... 1 ) = { 0 , 1 }

Proof

Step Hyp Ref Expression
1 1e0p1 1 = ( 0 + 1 )
2 1 oveq2i ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
3 0z 0 ∈ ℤ
4 fzpr ( 0 ∈ ℤ → ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
5 3 4 ax-mp ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
6 0p1e1 ( 0 + 1 ) = 1
7 6 preq2i { 0 , ( 0 + 1 ) } = { 0 , 1 }
8 2 5 7 3eqtri ( 0 ... 1 ) = { 0 , 1 }