Metamath Proof Explorer

Definition df-unif

Description: Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015)

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