Metamath Proof Explorer


Definition df-itv

Description: Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017) Use its index-independent form itvid instead. (New usage is discouraged.)

Ref Expression
Assertion df-itv Itv = Slot 1 6

Detailed syntax breakdown

Step Hyp Ref Expression
0 citv Itv
1 c1 1
2 c6 6
3 1 2 cdc 1 6
4 3 cslot Slot 1 6
5 0 4 wceq Itv = Slot 1 6