Metamath Proof Explorer


Definition df-unif

Description: Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015) Use its index-independent form unifid instead. (New usage is discouraged.)

Ref Expression
Assertion df-unif UnifSet = Slot 1 3

Detailed syntax breakdown

Step Hyp Ref Expression
0 cunif UnifSet
1 c1 1
2 c3 3
3 1 2 cdc 1 3
4 3 cslot Slot 1 3
5 0 4 wceq UnifSet = Slot 1 3